proposition: Lemma partialFlattening_desc : forall M (Mapp: isApp M) ML, isPartialFlattening ML (appBodyL Mapp) -> isPartialFlattening (ML ++ appBodyR Mapp :: nil) M.
proof: Proof. unfold isPartialFlattening. intros. destruct ML; try_solve. destruct ML; try_solve. rewrite (appUnits_app M Mapp). rewrite <- H. rewrite app_ass. auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)