proposition: Lemma horpo_args_var_consistent : forall M Ns, (forall L R, (subterm L M \/ (L = M /\ In R Ns)) -> L >> R -> envSubset (activeEnv R) (activeEnv L)) -> M [>>] Ns -> forall N', In N' Ns -> envSubset (activeEnv N') (activeEnv M).
proof: Proof. induction Ns; intros IH MNs N' N'Ns. inversion N'Ns. inversion N'Ns. inversion MNs; rewrite <- H. apply IH; trivial. right; auto with datatypes. destruct H3. apply env_subset_trans with (activeEnv x). inversion H5. apply IH; trivial. left; apply arg_subterm; trivial. apply env_subset_refl. apply activeEnv_subset_arg; trivial. apply IHNs; trivial. intros; apply IH; trivial. destruct H0; auto. right; destruct H0; split; auto with datatypes. inversion MNs; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)