proposition: Lemma equi_unifiable_decomp s t E: decomp s t = Some E -> [(s,t)] ≈ E.
proof: Proof. decomp_ind. - eauto with equi_unifiable. - easy. - eauto with equi_unifiable. - intros. now rewrite <-H1, <-H3, equi_unifiable_decompose_app. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)