proposition: Lemma beta_env_preserving : forall M N, M -b-> N -> env M = env N.
proof: Proof. intros. apply Red_env_preserving with BetaStep; trivial. apply betaStep_env_preserving. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)