proposition: Lemma AppL_app S1 S2 t: AppL (S1 ++ S2) t = AppL S1 (AppL S2 t).
proof: Proof. revert S2 t; induction S1; cbn; congruence. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)