proposition: Lemma AppR_app T1 T2 s: AppR s (T1 ++ T2) = AppR (AppR s T2) T1.
proof: Proof. revert T2 s; induction T1; cbn; congruence. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)