proposition: Lemma Lambda_ren delta n s: ren delta (Lambda n s) = Lambda n (ren (it n up_ren delta) s).
proof: Proof. induction n in delta |-*; cbn; (eauto 2). rewrite IHn. do 3 f_equal. symmetry. eapply it_commute. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)