proposition: Lemma algebraic_subst : forall M G (MG: correct_subst M G), algebraic M -> algebraicSubstitution G -> algebraic (subst MG).
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall G (MG: correct_subst M G), algebraic M -> algebraicSubstitution G -> algebraic (subst MG)). apply subterm_wf. clear M; intros M IH G MG Malg Galg. term_inv M. destruct (var_subst MG I) as [[W [p GpW MGterm]] | MGterm]. apply (@algebraic_morph_aux W (subst MG)). apply terms_conv_criterion; auto. apply env_comp_sym. apply subst_env_compat with p; trivial. apply (Galg p); trivial. apply AlgVar. apply var_is_var with x; rewrite MGterm; trivial. inversion Malg; try_solve. set (MGfunS := funS_subst_funS MG I). apply AlgFunApp; autorewrite with terms; trivial. apply funS_funApp; trivial. unfold isArg; rewrite appArgs_notApp; try_solve. assert (forall M, isFunS M -> ~isApp M). intro W; term_inv W. apply H3; trivial. apply AlgAbs with (abs_subst_abs (M:=Tr) I MG). destruct (abs_subst (M:=Tr) I MG). rewrite H0. apply IH; trivial. apply absBody_subterm. inversion Malg; try_solve. apply algebraicSubstitution_cons_none. apply algebraicSubstitution_lifted; trivial. destruct (isFunApp_dec Tr). apply AlgFunApp. apply funApp_subst_funApp; trivial. inversion Malg; try_solve. rewrite subst_type; simpl; trivial. intros. destruct (subst_arg_rev M' MG H) as [[Marg [MargM [MG' MargMG']]] | [p [T [Targ [TargT [GpT M'Targ_term]]]]]]. rewrite MargMG'. apply IH; trivial. apply arg_subterm; trivial. apply algebraic_arg with Tr; simpl; trivial. assert (M'Targ: M' ~ Targ). apply terms_conv_criterion; trivial. rewrite (appUnit_env Targ T). rewrite (appUnit_env M' (subst MG)). apply subst_env_compat with p; trivial. apply appArg_is_appUnit; trivial. apply appArg_is_appUnit; trivial. rewrite M'Targ. apply algebraic_arg with T; trivial. apply appArg_app with Targ; trivial. apply (Galg p); trivial. destruct (app_subst (M:=Tr) I MG). apply algebraic_app with (app_subst_app (M:=Tr) I MG). rewrite H. apply IH; trivial. apply appBodyL_subterm. apply algebraic_appBodyL; trivial. rewrite H0. apply IH; trivial. apply appBodyR_subterm. apply algebraic_appBodyR; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)