proposition: Lemma partialFlattening_app : forall M Ms, isPartialFlattening Ms M -> isApp M.
proof: Proof. intros M Ms Ms_pflat_M. unfold isPartialFlattening in *. repeat (destruct Ms; [contr | idtac]). case (isApp_dec M). auto. intro Mnapp. rewrite (appUnits_notApp M) in Ms_pflat_M. exfalso. eapply appUnits_notEmpty; eexact Ms_pflat_M. trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)