proposition: Lemma activeEnv_subset_partialFlattening : forall M N Ns, isPartialFlattening Ns N -> (forall N', In N' Ns -> 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 Ns, isPartialFlattening Ns N -> (forall N', In N' Ns -> envSubset (activeEnv N') (activeEnv M) ) -> envSubset (activeEnv N) (activeEnv M)). apply subterm_wf. clear N; intros N IH M Ns NsN H. set (Napp := partialFlattening_app N Ns NsN). rewrite (activeEnv_app N Napp). destruct (partialFlattening_inv N Napp Ns NsN) as [Ns_def | [Ns' [Ns'flat Ns_def]]]. apply env_subset_lsum. apply H. rewrite Ns_def; auto with datatypes. apply H. rewrite Ns_def; auto with datatypes. apply env_subset_lsum. apply IH with Ns'; trivial. apply appBodyL_subterm. intros. apply H. rewrite Ns_def; auto with datatypes. apply H. rewrite Ns_def; auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)