proposition: Lemma var_inclusion : forall t s, lt t s -> forall x, in_term_vars x t -> in_term_vars x s.
proof: Proof. intro t; induction t as [x | g ts HInd1] using term_ind_forall2. intros s Hts x0 Hx0. inversion Hx0. subst. lt_inversion Hts; subst; try inversion s_is. apply var_in; trivial. induction s as [x | f ss HInd2] using term_ind_forall2. intro Hst; lt_inversion Hst; try inversion s_is; try inversion t_is. intros Hts x x_in_t. lt_inversion Hts; try inversion s_is; try inversion t_is; subst. inversion x_in_t; subst. elim H1; clear H1; intros tx H1. elim H1; clear H1; intros tx_in_ss Htx. apply (HInd1 tx tx_in_ss (Fun g0 ts0) (Hsub tx tx_in_ss) x Htx). inversion x_in_t; subst. elim H1; clear H1; intros tx H1. elim H1; clear H1; intros tx_in_ss Htx. apply (HInd1 tx tx_in_ss (Fun g0 ts0)); trivial. apply Hsub; trivial. elim Ht'; clear Ht'; intro Ht'. constructor. exists t'; split; trivial. subst; trivial. constructor. exists t'. split; [hyp | apply (HInd2 t' t'_in_ts Ht' x x_in_t)]. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)