proposition: Lemma subst_comp : forall M G (MG: correct_subst M G), algebraic M -> CompSubst G -> algebraicSubstitution G -> CompH (subst MG).
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun (M: Term) => forall G (MG: correct_subst M G), algebraic M -> CompSubst G -> (forall i T, G |-> i/T -> algebraic T) -> CompH (subst MG)). apply subterm_wf. clear M; intros M IH G MG Mnorm Gcomp Gnorm. destruct M as [E Pt TM TypM]; simpl in * . destruct Pt as [?|?|A0 ?|??]. assert (Mvar: isVar (buildT TypM)). dependent inversion TypM; simpl; trivial. destruct (var_subst MG) as [[T [p GpT MGterm]] | MG_M]; trivial. apply horpo_comp_conv with T. apply Gcomp; trivial. apply nth_some_in with p; trivial. apply terms_conv_criterion; auto. apply env_comp_sym. apply subst_env_compat with p; trivial. apply horpo_var_comp; trivial. apply var_is_var with x; trivial. assert (termMG: term (subst MG) = term (buildT TypM)). apply funS_presubst. apply funS_is_funS with f; trivial. apply argsComp_appComp; term_inv (subst MG). apply funS_algebraic. simpl; inversion termMG. replace (f_type f) with (type (buildT TypM)). apply algebraic_funS; trivial. apply funS_is_funS with f; trivial. destruct TypM; try_solve. apply funS_is_funS with f; trivial. assert (Mabs: isAbs (buildT TypM)). apply abs_isAbs with A0 Pt; trivial. unfold CompH; apply horpo_comp_abs with (abs_subst_abs Mabs MG). apply algebraic_subst; trivial. intros S CS T TS Tcomp. destruct (abs_subst Mabs MG) as [MG_type MG_body]. set (CS_Mbody := subst_abs_c Mabs MG). assert (CSj : correct_subst (absBody Mabs) (Some T :: lift_subst G 1)). rewrite MG_body in CS. apply subst_disjoint_c with (subst_abs_c Mabs MG); trivial. apply singleton_correct_single with S; trivial. assert (CS_all: correct_subst (subst CS_Mbody) S). rewrite MG_body in CS; trivial. assert (S_Sj: subst CS = subst CSj). rewrite (subst_eq CS CS_all); trivial. set (CS_all' := singleton_correct_single CS_all TS). rewrite <- (singleton_subst CS_all' CS_all TS). apply subst_disjoint. rewrite S_Sj. apply IH. apply absBody_subterm. apply algebraic_absBody; trivial. intros Q Qin. case (in_inv Qin). intro Q_P. inversion Q_P; rewrite <- H0; trivial. intro Q_G. destruct (in_lift_subst Q G 1 Q_G) as [W W_G Q_lift_W]. rewrite Q_lift_W. unfold CompH; apply horpo_comp_lift. apply Gcomp; trivial. intros i W SW. destruct i. inversion SW. rewrite <- H0; apply horpo_comp_algebraic; trivial. inversion SW. destruct (var_subst_lift_rev G 1 H0) as [W' [GW' WW']]. rewrite WW'. apply algebraic_lift. apply (Gnorm i); trivial. set (M := buildT TypM) in * . assert (Mapp: isApp M). eapply app_isApp; simpl; trivial. destruct (app_subst Mapp MG) as [SL SR]. destruct (isFunApp_dec M). apply argsComp_appComp. apply algebraic_subst; trivial. apply funS_head_subst; trivial. intros P Parg. destruct (list_In_nth (tail (appUnits (subst MG))) P Parg) as [p unit_p]. assert (nth_error (appUnits (subst MG)) (S p) = Some P). destruct (appUnits (subst MG)); trivial. destruct p; try_solve. destruct (appUnits_subst_rev (S p) MG i H) as [P' [MP' PP']]. rewrite PP'. assert (P'arg_aux: nth_error (tail (appUnits M)) p = Some P'). inversion MP'. clear PP'; destruct (appUnits M); try_solve. assert (P'arg: isArg P' M). unfold isArg, appArgs. apply nth_some_in with p; trivial. apply IH; trivial. apply appUnit_subterm; trivial. apply appArg_is_appUnit; trivial. apply algebraic_arg with M; trivial. unfold CompH; apply horpo_comp_app with (app_subst_app Mapp MG). rewrite SL. apply IH; trivial. apply appBodyL_subterm. apply algebraic_appBodyL; trivial. rewrite SR. apply IH; trivial. apply appBodyR_subterm. apply algebraic_appBodyR; trivial. Qed.
imports: CoLoR(RelExtras ListExtras Horpo Computability PairLex HorpoComp LogicUtil)