proposition: Lemma Arr_app L1 L2 A: Arr (L1 ++ L2) A = Arr L1 (Arr L2 A).
proof: Proof. induction L1; cbn; congruence. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)