proposition: Lemma decomp_none_ind (P: exp X -> exp X -> Type): (forall x t, const x <> t -> ~ isVar t -> P (const x) t) -> (forall x t, const x <> t -> ~ isVar t -> P t (const x)) -> (forall s t, lambda s <> t -> P (lambda s) t) -> (forall s t, s <> lambda t -> P s (lambda t)) -> (forall s1 s2 t1 t2, s1 s2 <> t1 t2 -> P s1 t1 -> P (s1 s2) (t1 t2)) -> (forall s1 s2 t1 t2, s1 s2 <> t1 t2 -> P s2 t2 -> P (s1 s2) (t1 t2)) -> forall s t, decomp s t = None -> P s t.
proof: Proof. intros H1 H2 H3 H4 IH1 IH2 s t; induction s in t |-*; cbn. all: destruct eq_dec; try discriminate. all: destruct t; try discriminate; eauto. destruct decomp eqn: D1; [destruct (decomp s2 t2) eqn: D2|]; try discriminate. all: 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)