proposition: Lemma beta_var_consistent : forall M N, M -b-> N -> envSubset (activeEnv N) (activeEnv M).
proof: Proof. intros. apply red_var_consistent with BetaStep; trivial. clear M N H; intros M N MN. destruct MN. rewrite activeEnv_lower. rewrite (activeEnv_app M Mapp). rewrite (activeEnv_abs (appBodyL Mapp) MLabs). destruct (isVarDecl_dec (activeEnv (absBody MLabs)) 0) as [[B Ml0] | Mln]. assert (Mlb0: exists A, activeEnv (absBody MLabs) |= 0 := A). exists B; trivial. rewrite (singleton_subst_activeEnv_subst (beta_subst M Mapp MLabs) (singletonSubst_cond (lift (appBodyR Mapp) 1)) Mlb0). rewrite (activeEnv_lift (appBodyR Mapp) 1). simpl; autorewrite with datatypes using unfold loweredEnv; simpl. apply env_subset_refl. rewrite (singleton_subst_activeEnv_noSubst (beta_subst M Mapp MLabs) Mln (singletonSubst_cond (lift (appBodyR Mapp) 1))); trivial. unfold loweredEnv; autorewrite with datatypes using simpl. apply env_subset_sum_l. simpl. apply env_comp_subset with (tail (env (subst (beta_subst M Mapp MLabs)))) (env (appBodyR Mapp)). autorewrite with terms datatypes using simpl; auto with terms. apply env_subset_tail; apply activeEnv_subset. apply activeEnv_subset. rewrite finalSeg1_tail. apply env_subset_refl. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)