proposition: Lemma partialFlattening_subterm : forall M Ms m, isPartialFlattening Ms M -> In m Ms -> subterm m M.
proof: Proof. intros M Ms m Ms_pflat m_Ms. assert (Mapp: isApp M). apply partialFlattening_app with Ms; trivial. unfold isPartialFlattening in *. repeat (destruct Ms; [contr | idtac]). destruct m_Ms as [m_t | [m_t0 | m_Ms]]. apply partialFlattening_subterm_aux with (t0::Ms). auto with datatypes. rewrite <- m_t; trivial. apply appUnit_subterm; trivial. unfold isAppUnit; rewrite <- m_t0; rewrite <- Ms_pflat. auto with datatypes. apply appUnit_subterm; trivial. unfold isAppUnit; rewrite <- Ms_pflat; auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)