proposition: Lemma activeEnv_subset_unit : forall Mu M, isAppUnit Mu M -> envSubset (activeEnv Mu) (activeEnv M).
proof: Proof. destruct M as [E Pt T M]; induction M. intros; rewrite (appUnit_notApp (buildT (TVar v)) Mu); auto with terms. apply env_subset_refl. intros; rewrite (appUnit_notApp (buildT (TFun E f)) Mu); auto with terms. apply env_subset_refl. intros; rewrite (appUnit_notApp (buildT (TAbs M)) Mu); auto with terms. apply env_subset_refl. intros. rewrite (@activeEnv_app (buildT (TApp M1 M2)) I). destruct (appUnit_app Mu (buildT (TApp M1 M2)) I); trivial. rewrite H0. apply env_subset_sum_r; apply env_subset_refl. apply env_subset_sum_l. apply activeEnv_app_comp. apply IHM1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)