proposition: Lemma AppL_ren delta S t: ren delta (AppL S t) = AppL (renL delta S) (ren delta t).
proof: Proof. induction S; cbn; congruence. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)