def Term.is_lam : Term → Bool

Equations

• (:λ[a] a_1).is_lam = true
• x✝.is_lam = false

inductive Value : Term → Prop

• var {x : Nat} : Value #x
• app {f a : Term} : Value f → Value a → ¬f.is_lam = true → Value (f :@ a)
• lam {t : Term} {A : Ty} : Value t → Value (:λ[A] t)

theorem value_sound {t : Term} : Value t → ∀ (t' : Term), ¬t ~> t'

inductive VarSpine : Term → Prop

• var {x : Nat} : VarSpine #x
• app {h t : Term} : VarSpine h → Value t → VarSpine (h :@ t)

theorem var_spine_not_lam {t : Term} : VarSpine t → ¬t.is_lam = true

theorem lam_value {Γ : List Ty} {t : Term} {A B : Ty} : Γ ⊢ t : (A -t> B) → Value t → (∃ (b : Term), t = :λ[A] b) ∨ VarSpine t

theorem progress (t : Term) : Value t ∨ ∃ (t' : Term), t ~> t'