proposition: Lemma preservation_under_steps s s' Gamma A: s >* s' -> Gamma ⊢ s : A -> Gamma ⊢ s' : A.
proof: Proof. induction 1 in Gamma, A |-*; eauto using preservation_under_reduction. Qed.
imports: List Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics)