theorem preservation_step {Γ : List Ty} {A : Ty} {t t' : Term} : Γ ⊢ t : A → t ~> t' → Γ ⊢ t' : A

theorem preservation {Γ : List Ty} {A : Ty} {t t' : Term} : Γ ⊢ t : A → LeanSubst.Star Red t t' → Γ ⊢ t' : A