proposition: Lemma Unifies_app sigma E1 E2: Unifies sigma (E1 ++ E2) <-> Unifies sigma E1 /\ Unifies sigma E2.
proof: Proof. induction E1; cbn; simplify; intuition easy. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)