proposition: Lemma appUnits_subst_rev : forall M G i W' (MG: correct_subst M G), isFunS (appHead M) -> nth_error (appUnits (subst MG)) i = Some W' -> exists W, exists Mi: nth_error (appUnits M) i = Some W, W' = subst (appUnits_subst_c i MG Mi).
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall G i W' (MG: correct_subst M G), isFunS (appHead M) -> nth_error (appUnits (subst MG)) i = Some W' -> exists W, exists Mi: nth_error (appUnits M) i = Some W, W' = subst (appUnits_subst_c i MG Mi)). apply subterm_wf. clear M; intros M IH G i W' MG M_fapp W'arg. destruct (isApp_dec M) as [Mapp | Mnapp]. set (MG_app := app_subst_app Mapp MG). set (W''arg := W'arg). rewrite (appUnits_app (subst MG) MG_app) in W''arg. destruct (app_subst Mapp MG). set (MGl := subst (subst_appL_c Mapp MG)) in * . set (MGr := subst (subst_appR_c Mapp MG)) in * . replace (appBodyL MG_app) with MGl in W''arg. replace (appBodyR MG_app) with MGr in W''arg. assert (ML_head: isFunS (appHead (appBodyL Mapp))). rewrite (appHead_app M Mapp) in M_fapp; trivial. destruct (nth_app (appUnits MGl) (MGr::nil) i W''arg) as [[MGl_i i_l] | [MGr_i i_r]]. destruct (IH (appBodyL Mapp) (appBodyL_subterm M Mapp) G i W' (subst_appL_c Mapp MG)) as [W [Mi W'def]]; trivial. exists W. assert (M_i: nth_error (appUnits M) i = Some W). rewrite (appUnits_app M Mapp). rewrite nth_app_left; trivial. rewrite <- (appUnits_subst_length (subst_appL_c Mapp MG)); trivial. exists M_i. rewrite W'def; trivial. apply term_eq; autorewrite with datatypes terms using trivial. exists (appBodyR Mapp). destruct (nth_error_singleton_in MGr (i - length (appUnits MGl)) MGr_i). assert (i = length (appUnits MGl)). lia. assert (Mi: nth_error (appUnits M) i = Some (appBodyR Mapp)). rewrite (appUnits_app M Mapp). rewrite nth_app_right. rewrite H3. rewrite <- (appUnits_subst_length (subst_appL_c Mapp MG)); trivial. fold MGl; rewrite Nat.sub_diag; trivial. rewrite H3. rewrite <- (appUnits_subst_length (subst_appL_c Mapp MG)); trivial. fold MGl; auto. exists Mi. destruct (nth_error_singleton_in MGr (i - length (appUnits MGl)) MGr_i). rewrite <- H4. unfold MGr; apply subst_proof_irr. term_inv M. exists Tr. rewrite appUnits_notApp in W'arg. destruct i. inversion W'arg. simpl. assert (Some (buildT (TFun E f)) = Some Tr); trivial. exists H. apply term_eq; autorewrite with terms using trivial. simpl in W'arg. destruct i; try_solve. assert (forall M, isFunS M -> isApp M -> False). intro M; term_inv M. intro MG_app; apply H with (subst MG); trivial. apply funS_subst_funS; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)