proposition: Lemma partialFlattening_conv : forall M Ms N Q, M ~(Q) N -> isPartialFlattening Ms M -> exists Ns, isPartialFlattening Ns N /\ conv_list Ms Ns Q.
proof: Proof. destruct M as [E Pt T M]; induction M; intros. set (w := partialFlattening_app (buildT (TVar v)) Ms H0); try_solve. set (w := partialFlattening_app (buildT (TFun E f)) Ms H0); try_solve. set (w := partialFlattening_app (buildT (TAbs M)) Ms H0); try_solve. assert (Napp: isApp N). assert (H' : (buildT (TApp M1 M2)) ~ N) by (exists Q; trivial). rewrite <- H'; simpl; trivial. destruct (partialFlattening_inv (buildT (TApp M1 M2)) I Ms) as [Ms_def | [Ms' [Ms'l MsMs']]]; trivial. exists (appBodyL Napp :: appBodyR Napp :: nil); split. unfold isPartialFlattening; rewrite (appUnits_app N Napp); trivial. rewrite Ms_def. constructor. apply app_conv_app_left_aux; trivial. constructor. apply app_conv_app_right_aux; trivial. constructor. destruct (IHM1 Ms' (appBodyL Napp) Q) as [Ns' [Ns'Nl Ms'Ns']]; trivial. change (buildT M1) with (@appBodyL (buildT (TApp M1 M2)) I). apply app_conv_app_left_aux; trivial. exists (Ns' ++ appBodyR Napp :: nil); split. unfold isPartialFlattening. destruct Ns'; try solve [inversion Ns'Nl]. destruct Ns'; try solve [inversion Ns'Nl]. simpl in * ; rewrite app_comm_cons. rewrite <- app_ass; rewrite Ns'Nl. sym; apply appUnits_app. rewrite MsMs'. unfold conv_list; apply list_sim_app; trivial. constructor. apply app_conv_app_right_aux; trivial. constructor. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)