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