proposition: Lemma decomp'_none_ind (P: eqs X -> Type): (forall E s t, decomp s t = None -> P ((s, t) :: E)) -> (forall E s t, P E -> P ((s, t) :: E)) -> forall E, decomp' E = None -> P E.
proof: Proof. intros H IH; induction E as [| [s t]]; cbn; try discriminate. destruct decomp eqn: EQ1; [destruct decomp' eqn: EQ2 |]; try discriminate. all: intros _. eapply IH; intuition easy. now eapply H. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)