proposition: Lemma var_in_s_in_terms_greater_than_s : forall t s, le_mpo t s -> forall x, in_term_vars x t -> in_term_vars x s.
proof: Proof. intros t s H; elim H; clear H; intro H. subst t; trivial. revert s H. induction t as [x | g ts HInd1] using term_ind_forall2. intros s Hts x0 Hx0. inversion Hx0. subst. inversion Hts; subst. elim H; clear H; intros s Hs; elim Hs; clear Hs; intros s_in_ss Hss. apply var_in; trivial. induction s as [x | f ss HInd2] using term_ind_forall2. intro Hst; inversion Hst. intros Hts x x_in_t. inversion Hts as [f' g' ss' ts' ltFfg H H' | f' ss' ts' Hss'ts' | f' ss' t' Hex]; subst. inversion x_in_t; subst. elim H2; clear H2; intros tx H2. elim H2; clear H2; intros tx_in_ts Htx. apply (HInd1 tx tx_in_ts (Fun f ss) (H tx tx_in_ts) x Htx). inversion x_in_t; subst. elim H1; clear H1; intros tx H1. elim H1; clear H1; intros tx_in_ts Htx. apply (HInd1 tx tx_in_ts (Fun f ss)); trivial. elim (mult2element (transp lt_mpo) IN_eqA_compat ts ss Hss'ts' tx tx_in_ts). intros s Hs; elim Hs; clear Hs; intros s_in_ss Hs. constructor 3. exists s; split; trivial. elim Hex; clear Hex; intros sx Hex. elim Hex; clear Hex; intros sx_in_ss Hsx. elim Hsx; clear Hsx; intro Hsx. constructor. exists sx. subst sx; split; trivial. constructor. exists sx. split; [hyp | apply (HInd2 sx sx_in_ss Hsx x x_in_t)]. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)