proposition: Lemma partialFlattening_env : forall M Ms, isPartialFlattening Ms M -> forall Min, In Min Ms -> env Min = env M.
proof: Proof. intros. destruct Ms; try_solve. destruct Ms; try_solve. destruct H0. rewrite <- H0. destruct (head_notNil (appUnits_not_nil t)). destruct (head_notNil (appUnits_not_nil M)). rewrite <- (appUnit_env x t). rewrite <- (appUnit_env x0 M). rewrite (list_decompose_head (appUnits_not_nil t) e) in H. rewrite (list_decompose_head (appUnits_not_nil M) e0) in H. inversion H; trivial. unfold isAppUnit; destruct (appUnits M); inversion e0; try_solve. unfold isAppUnit; destruct (appUnits t); inversion e; try_solve. apply appUnit_env. unfold isAppUnit; rewrite <- H. destruct H0. rewrite <- H0; firstorder auto with datatypes. firstorder auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)