proposition: Lemma subst_list_partialFlattening : forall M Ms G (MG: correct_subst M G), isPartialFlattening Ms M -> exists Ns, isPartialFlattening Ns (subst MG) /\ subst_list Ms Ns G.
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall Ms G (MG: correct_subst M G), isPartialFlattening Ms M -> exists Ns, isPartialFlattening Ns (subst MG) /\ subst_list Ms Ns G). apply subterm_wf. clear M; intros M IH Ms G MG MsM. set (Mapp := partialFlattening_app M Ms MsM). set (MGapp := app_subst_app Mapp MG). destruct (app_subst Mapp MG). destruct (partialFlattening_inv M Mapp Ms MsM). exists (appBodyL MGapp :: appBodyR MGapp :: nil). split. unfold isPartialFlattening; rewrite (appUnits_app (subst MG) MGapp); trivial. rewrite H1; constructor. exists (subst_appL_c Mapp MG); trivial. constructor. exists (subst_appR_c Mapp MG); trivial. constructor. destruct H1 as [MsL [MsLflat Ms_def]]. destruct (IH (appBodyL Mapp) (appBodyL_subterm M Mapp) MsL G (subst_appL_c Mapp MG)) as [NsL [NsL_flat MsLNsL]]; trivial. exists (NsL ++ appBodyR MGapp :: nil). constructor. apply (partialFlattening_desc (subst MG) MGapp); trivial. unfold MGapp; rewrite H; trivial. rewrite Ms_def. unfold subst_list; apply list_sim_app; trivial. constructor. exists (subst_appR_c Mapp MG); trivial. constructor. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)