proposition: Lemma activeEnv_subset_units : forall M N, (forall N', In N' (appUnits N) -> envSubset (activeEnv N') (activeEnv M)) -> envSubset (activeEnv N) (activeEnv M).
proof: Proof. intros M N; gen M; clear M. apply well_founded_ind with (R := subterm) (P := fun N => forall M, (forall N', In N' (appUnits N) -> envSubset (activeEnv N') (activeEnv M) ) -> envSubset (activeEnv N) (activeEnv M)). apply subterm_wf. clear N; intros N IH M H. destruct (isApp_dec N) as [Napp | Nnapp]. rewrite (activeEnv_app N Napp). apply env_subset_lsum. apply IH. apply appBodyL_subterm. intros. apply H. fold (isAppUnit N' N). apply appUnit_left with Napp; trivial. apply H. apply appArg_is_appUnit. apply appArg_right with Napp; trivial. apply H. rewrite appUnits_notApp; auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)