proposition: Lemma equi_unifiable_comm s t: [(s, t)] ≈ [(t, s)].
proof: Proof. intros ?; simplify; cbn; intuition (auto with relations). Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)