proposition: Lemma preservation_under_reduction s s' Gamma A: s > s' -> Gamma ⊢ s : A -> Gamma ⊢ s' : A.
proof: Proof. induction 1 in Gamma, A |-*; intros H1; invp @typing; eauto. inv H3. eapply preservation_under_substitution; eauto. intros []; cbn; eauto. intros ? H; now injection H as ->. Qed.
imports: List Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics)