proposition: Lemma allPartialFlattenings : forall M, isApp M -> { MF: list (list Term) | forall Mpf, isPartialFlattening Mpf M <-> In Mpf MF }.
proof: Proof. destruct M as [E Pt T M]; induction M; try_solve. intros _. destruct (isApp_dec (buildT M1)). destruct IHM1; trivial. set (F0 := buildT M1::buildT M2::nil). set (fp := (fun l => l ++ buildT M2::nil)). set (Fr := map fp x). exists (F0::Fr); split; intro. destruct (partialFlattening_inv (buildT (TApp M1 M2)) I Mpf H). rewrite H0; unfold F0; try_solve. destruct H0 as [Ns [NsL MpfNs]]. rewrite MpfNs. right; unfold Fr. set (Nsx := proj1 (i0 Ns) NsL). destruct (list_In_nth x Ns Nsx) as [p xp]. apply nth_some_in with p. simpl. change (Ns ++ buildT M2::nil) with (fp Ns). apply nth_map_some; trivial. inversion H. rewrite <- H0. unfold F0; simpl. rewrite (appUnits_app (buildT (TApp M1 M2)) I); trivial. destruct (list_In_nth Fr Mpf H0) as [p xp]. unfold Fr in xp. destruct (nth_map_some_rev x p fp xp) as [w [xpw fpw]]. rewrite <- fpw; unfold fp. change (buildT M2) with (appBodyR (M:=buildT (TApp M1 M2)) I). apply partialFlattening_desc. apply (proj2 (i0 w)). apply nth_some_in with p; trivial. exists ((buildT M1::buildT M2::nil)::nil). split; intros. destruct (partialFlattening_inv (buildT (TApp M1 M2)) I Mpf H). try_solve. destruct H0 as [Ns [NsL _]]. absurd (isApp (buildT M1)); trivial. apply partialFlattening_app with Ns; trivial. unfold isPartialFlattening. inversion H; try_solve. rewrite <- H0; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)