proposition: Lemma Red_env_preserving : forall M N, Red M N -> env M = env N.
proof: Proof. intros M N MN. induction MN; try solve [term_inv M; term_inv N]. apply R_env_preserving; trivial. term_inv M; term_inv N; inversion IHMN; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubstConv)