proposition: Lemma betaStep_env_preserving : forall M N, BetaStep M N -> env M = env N.
proof: Proof. intros. inversion H. rewrite lower_env. rewrite beta_env. unfold loweredEnv, finalSeg; simpl. rewrite initialSeg_full; trivial. lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)