proposition: Lemma beta_env : forall M (Mapp: isApp M) (MLabs: isAbs (appBodyL Mapp)), env (subst (beta_subst M Mapp MLabs)) = None :: env M.
proof: Proof. intros. rewrite subst_env; simpl. unfold subst_ran; simpl. rewrite lift_env; simpl. unfold liftedEnv; simpl. rewrite absBody_env; simpl. rewrite appBodyL_env; simpl. rewrite finalSeg_full; simpl. rewrite appBodyR_env; simpl. rewrite env_sub_empty. rewrite env_sum_double; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)