proposition: Lemma decomp'_some_var e E E': decomp' E = Some (e :: E') -> exists x, fst e = var x .
proof: Proof. remember (e :: E') as E''. intros H; revert H e E' HeqE''; decomp_ind; intros. - discriminate. - destruct E1; eauto; injection HeqE'' as ? ?; subst; eauto. eapply decomp_some_var in H; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)