proposition: Lemma decomp_some_ind (P: exp X -> exp X -> eqs X -> Type): (forall s, P s s nil) -> (forall x s, var x <> s -> P (var x) s [(var x, s)]) -> (forall x s, var x <> s -> P s (var x) [(var x, s)]) -> (forall s1 s2 t1 t2 E1 E2, s1 s2 <> t1 t2 -> decomp s1 t1 = Some E1 -> P s1 t1 E1 -> decomp s2 t2 = Some E2 -> P s2 t2 E2 -> P (s1 s2) (t1 t2) (E1 ++ E2)) -> forall s t E, decomp s t = Some E -> P s t E.
proof: Proof. intros H1 H2 H3; induction s; intros [] E; cbn. all: destruct eq_dec as [EQ|NEQ]; try discriminate. 1 - 11: injection 1 as ?; subst E; eauto. 1 - 4: injection EQ; intros; subst; eauto. destruct (decomp s1 e) eqn: EQ1; try discriminate. destruct (decomp s2 e0) eqn: EQ2; try discriminate. injection 1 as ?; subst. eapply X0; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)