proposition: Lemma listtyping_preservation_under_renaming delta Gamma Delta S L: Gamma ⊢₊ S : L -> Delta ⊫ delta : Gamma -> Delta ⊢₊ renL delta S : L.
proof: Proof. intros H1 H2; induction H1; cbn; (eauto 3). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)