proposition: Lemma decomp_some_var s t e E: decomp s t = 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. - injection HeqE' as ? ?; subst; eexists; cbn; eauto. - injection HeqE' as ? ?; subst; eexists; cbn; eauto. - destruct E1; eauto; injection HeqE' as ? ?; subst; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)