proposition: Lemma equi_unifiable_decomp' E E': decomp' E = Some E' -> E ≈ E'.
proof: Proof. decomp_ind; intuition (auto with relations). now rewrite <-H1, <-equi_unifiable_decomp with (E := E1); eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)