inductive value : Trm → Prop

• value_abs (e : Trm) (T : Typ) : (λ T,e).lc → value (λ T,e)

theorem value_regular (t : Trm) : value t → t.lc

inductive eval : Trm → Trm → Prop

• eval_beta (e1 e2 : Trm) (T : Typ) : (λ T,e1).lc → value e2 → eval ((λ T,e1) @ e2) (e1.open₀ e2)
• eval_app1 (e1 e1' e2 : Trm) : e2.lc → eval e1 e1' → eval (e1 @ e2) (e1' @ e2)
• eval_app2 (e1 e2 e2' : Trm) : e1.lc → eval e2 e2' → eval (e1 @ e2) (e1 @ e2')

theorem eval_regular (e1 e2 : Trm) : eval e1 e2 → e1.lc ∧ e2.lc

theorem preservation (E : context) (e : Trm) (T : Typ) : typing E e T → ∀ (e' : Trm), eval e e' → typing E e' T

theorem progress (e : Trm) (T : Typ) : typing [] e T → value e ∨ ∃ (e' : Trm), eval e e'