proposition: Lemma horpo_RC_env_preserving : forall M N, M >>= N -> env M = env N.
proof: Proof. intros. inversion H. apply horpo_env_preserving; trivial. trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)