proposition: Lemma horpo_var_consistent : forall M N, M >> N -> envSubset (activeEnv N) (activeEnv M).
proof: Proof. intros M N. assert (Res: forall P, fst P >> snd P -> envSubset (activeEnv (snd P)) (activeEnv (fst P))). intro P. apply well_founded_ind with (R := LexProd_Lt) (P := fun P => fst P >> snd P -> envSubset (activeEnv (snd P)) (activeEnv (fst P))). apply lexprod_wf. unfold ltL, gtR, subterm_gt. rewrite transp_invol. apply subterm_wf. unfold ltR, gtR, subterm_gt. rewrite transp_invol. apply subterm_wf. clear M N P. intros P IH MN. destruct P as [M N]; simpl in * . apply horpo_var_consistent_aux; trivial. intros. apply (IH (M', N')). destruct H. constructor; exact H. destruct H; rewrite H. constructor 2; trivial. auto with sets. simpl; trivial. intros. apply (Res (M, N)); trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)