proposition: Lemma ordertyping_preservation_under_renaming n delta Gamma Delta s A: Gamma ⊢(n) s : A -> Delta ⊫ delta : Gamma -> Delta ⊢(n) ren_exp delta s : A.
proof: Proof. intros; eapply ordertyping_weak_preservation_under_renaming; eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)