proposition: Lemma acc_app_acc_L : forall M (Mapp: isApp M), algebraic (appBodyL Mapp) -> algebraic (appBodyR Mapp) -> AccR M -> AccR (appBodyL Mapp).
proof: Proof. intros; unfold AccR. apply Acc_mimic with M (fun M N => exists Mapp: isApp M, algebraic (appBodyL Mapp) /\ algebraic (appBodyR Mapp) /\ appBodyL Mapp = N); try solve [trivial | exists Mapp; split; trivial]. unfold transp; clear H H0 H1 M Mapp; intros M M' MM' N' M'N'. destruct MM' as [Mapp [MLnorm [MRnorm MM']]]. assert (envOk: env N' = env (appBodyR Mapp)). term_inv M. replace E with (env M'). sym; auto with comp. rewrite <- MM'; auto. assert (typArrow: isArrowType (type N')). rewrite <- (R_type_preserving M'N'), <- MM'; term_inv M. assert (typCorrect: type_left (type N') = type (appBodyR Mapp)). rewrite <- (R_type_preserving M'N'), <- MM'; term_inv M. set (Ncond := Build_appCond N' (appBodyR Mapp) envOk typArrow typCorrect). set (N := buildApp Ncond). exists N. set (Napp := buildApp_isApp Ncond). apply R_right_app_monotonous with M' N' Mapp Napp; trivial. rewrite <- MM'; trivial. unfold N, Napp; rewrite buildApp_Lok; trivial. unfold N, Napp; rewrite buildApp_Rok; trivial. exists (buildApp_isApp Ncond); split. unfold N; rewrite buildApp_Lok; trivial. apply R_algebraic_preserving with M'; trivial. rewrite <- MM'; trivial. simpl; split. unfold N; rewrite buildApp_Rok; trivial. unfold N; rewrite buildApp_Lok; trivial. exists Mapp; split; trivial. split; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)