proposition: Lemma preservation_under_substitution sigma Gamma Delta s A: Gamma ⊢ s : A -> Delta ⊩ sigma: Gamma -> Delta ⊢ sigma • s : A.
proof: Proof. induction 1 in sigma, Delta |-*; intros H'; cbn [subst_exp]; subst; eauto. econstructor; apply IHtyping; intros []; cbn; eauto. intros; eapply preservation_under_renaming; eauto. intros ?; eauto. Qed.
imports: List Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics)