proposition: Lemma subst_list_units : forall M G (MG: correct_subst M G), isFunS (appHead M) -> subst_list (appUnits M) (appUnits (subst MG)) G.
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall G (MG: correct_subst M G), isFunS (appHead M) -> subst_list (appUnits M) (appUnits (subst MG)) G). apply subterm_wf. clear M; intros M IH G MG Mhead. destruct (isApp_dec M) as [Mapp | Mnapp]. destruct (app_subst Mapp MG); trivial. rewrite (appUnits_app M Mapp). rewrite (appUnits_app (subst MG) (app_subst_app Mapp MG)). unfold subst_list; apply list_sim_app. rewrite H. apply (IH (appBodyL Mapp)). apply appBodyL_subterm. apply appHead_left; trivial. constructor. exists (subst_appR_c Mapp MG). destruct (app_subst Mapp MG); trivial. constructor. rewrite appUnits_notApp; try_solve. rewrite appUnits_notApp. constructor. exists MG; trivial. constructor. term_inv M. assert (isFunS (subst MG)). apply funS_subst_funS; trivial. term_inv (subst MG). Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)