proposition: Lemma notFunApp_subst : forall M G (MG: correct_subst M G), isApp M -> algebraicSubstitution G -> ~isFunApp M -> ~isFunApp (subst MG).
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall G (MG: correct_subst M G), isApp M -> algebraicSubstitution G -> ~isFunApp M -> ~isFunApp (subst MG) ). apply subterm_wf. clear M; intros M IH G MG Mapp Galg Mnfa MGfa. destruct (app_subst Mapp MG). set (MGapp := app_subst_app Mapp MG). destruct (term_case (appBodyL Mapp)) as [[[MLvar | MLfun] | MLabs] | MLapp]. destruct (var_subst (subst_appL_c Mapp MG)) as [[T [y GyT MGterm]] | MGterm]; trivial. absurd (isBaseType (type (appBodyL MGapp))). assert (forall W (Wapp: isApp W), ~isBaseType (type (appBodyL Wapp))). intros; term_inv W. apply H1. apply algebraic_funApp_datatype. apply algebraic_morph_aux with T. trivial. apply terms_conv_criterion. rewrite appBodyL_env. apply env_comp_sym. apply subst_env_compat with y; trivial. rewrite <- MGterm; rewrite <- H; trivial. apply (Galg y); trivial. apply isFunApp_left; trivial. absurd (isFunS (appHead (subst MG))). assert (forall W, isVar W -> ~isFunS W). intro W; term_inv W. apply H1. rewrite (appHead_app (subst MG) MGapp). assert (isVar (appBodyL MGapp)). assert (forall W, isVar W -> exists x, term W = %x). intro W; term_inv W. exists x; trivial. destruct (H2 (appBodyL Mapp) MLvar). apply var_is_var with x. unfold MGapp; rewrite H. rewrite MGterm; trivial. rewrite appHead_notApp; trivial. assert (forall W, isVar W -> ~isApp W). intro W; term_inv W. apply H3; trivial. trivial. absurd (isFunApp M); trivial. unfold isFunApp in * . rewrite (appHead_app M Mapp); simpl. rewrite (appHead_notApp (appBodyL Mapp)); trivial. assert (forall W, isFunS W -> ~isApp W). intro W; term_inv W. apply H1; trivial. unfold isFunApp in * . rewrite (appHead_app (subst MG) MGapp) in MGfa. rewrite (appHead_notApp (appBodyL MGapp)) in MGfa. unfold MGapp in MGfa; rewrite H in MGfa. assert (forall W, isFunS W -> isAbs W -> False). intro W; term_inv W. apply H1 with (subst (subst_appL_c Mapp MG)); trivial. apply abs_subst_abs; trivial. apply abs_isnot_app; trivial. unfold MGapp. rewrite H. apply abs_subst_abs; trivial. absurd (isFunApp (appBodyL MGapp)); trivial. unfold MGapp; rewrite H. apply IH; trivial. apply appBodyL_subterm. apply notFunApp_left_inv; trivial. apply isFunApp_left; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)