proposition: Lemma red_var_consistent : forall M N, Red M N -> envSubset (activeEnv N) (activeEnv M).
proof: Proof. induction 1; intros. apply step_var_consistent; trivial. rewrite (activeEnv_app M Mapp). rewrite (activeEnv_app N Napp). rewrite H0. apply env_subset_sum_req; trivial. rewrite (activeEnv_app M Mapp). rewrite (activeEnv_app N Napp). rewrite H0. apply env_subset_sum_leq; trivial. rewrite <- H0. apply activeEnv_app_comp. rewrite (activeEnv_abs M Mabs). rewrite (activeEnv_abs N Nabs). intros x A D. apply varD_tail. apply IHReduction. apply varD_tail_rev; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubstConv)