proposition: Lemma partialFlattening_inv : forall M (Mapp: isApp M) Ms, isPartialFlattening Ms M -> Ms = appBodyL Mapp :: appBodyR Mapp :: nil \/ exists Ns, isPartialFlattening Ns (appBodyL Mapp) /\ Ms = Ns ++ appBodyR Mapp :: nil.
proof: Proof. destruct M as [E Pt T M]; induction M; intros. set (w := partialFlattening_app (buildT (TVar v)) Ms H); try_solve. set (w := partialFlattening_app (buildT (TFun E f)) Ms H); try_solve. set (w := partialFlattening_app (buildT (TAbs M)) Ms H); try_solve. destruct Ms. inversion H. destruct Ms. inversion H. unfold isPartialFlattening in H. rewrite (appUnits_app (buildT (TApp M1 M2)) I) in H. destruct Ms. left. destruct (app_inj_tail (appUnits t) (appUnits (appBodyL Mapp)) t0 (appBodyR Mapp)); trivial. rewrite H1. rewrite (eq_units_eq_terms t (appBodyL Mapp) H0); trivial. right. assert (MLapp: isApp (appBodyL Mapp)). destruct (isApp_dec (appBodyL Mapp)); trivial. rewrite (appUnits_notApp (appBodyL (M:=buildT (TApp M1 M2)) I)) in H; trivial. simpl in H. exfalso; cut (appUnits t <> nil). destruct (appUnits t); auto. inversion H. cut (length (l ++ t0 :: t1 :: Ms) = length (buildT M2 :: nil)). autorewrite with datatypes; simpl; lia. rewrite H2; trivial. apply appUnits_not_nil. exists (t :: t0 :: dropLast (t1 :: Ms)); split. set (w := dropLast_eq H). rewrite dropLast_last in w. set (ww := dropLast_app). rewrite dropLast_app in w. simpl in w; trivial. simpl; rewrite (appUnits_app (buildT M1) MLapp); auto with datatypes. set (w := last_eq H). simpl in w. rewrite last_app in w. rewrite last_app in w. change ((t :: t0 :: dropLast (t1 :: Ms)) ++ appBodyR Mapp :: nil) with (t :: t0 :: (dropLast (t1 :: Ms) ++ buildT M2 :: nil)). rewrite dropLast_plus_last; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)