proposition: Lemma decomp'_some_ind (P: eqs X -> eqs X -> Prop): P nil nil -> (forall s t E E1 E2, decomp s t = Some E1 -> decomp' E = Some E2 -> P E E2 -> P ((s, t) :: E) (E1 ++ E2)) -> forall E E', decomp' E = Some E' -> P E E'.
proof: Proof. intros H IH; induction E as [| [s t]]; cbn. - now injection 1 as <-. - intros E'; destruct decomp eqn: H1; destruct decomp' eqn: H2; try discriminate. intros [= <-]; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)