proposition: Lemma horpo_app_reduct : forall M N (Mapp: isApp M), M >> N -> ~isFunApp M \/ isArrowType (type M) -> (exists MLabs: isAbs (appBodyL Mapp), N = lower (subst (beta_subst M Mapp MLabs)) (beta_lowering M Mapp MLabs)) \/ exists Napp: isApp N, (appBodyL Mapp = appBodyL Napp /\ appBodyR Mapp >> appBodyR Napp) \/ (appBodyL Mapp >> appBodyL Napp /\ appBodyR Mapp = appBodyR Napp) \/ (appBodyL Mapp >> appBodyL Napp /\ appBodyR Mapp >> appBodyR Napp).
proof: Proof. intros. destruct H. assert (~isFunApp M). destruct H0; trivial. apply algebraic_arrowType; trivial. destruct H4; try_solve. absurd (isFunApp M); trivial. unfold isFunApp; apply funS_is_funS with f; trivial. absurd (isFunApp M); trivial. unfold isFunApp; apply funS_is_funS with f; trivial. right. exists NApp. inversion H7. rewrite (app_proof_irr M Mapp MApp). destruct (horpo_app M N MApp NApp H) as [LL [RR [Ls | Rs]]]; trivial. inversion RR. right; right; split; trivial. right; left; split; trivial. inversion LL. right; right; split; trivial. left; split; trivial. term_inv M. destruct (beta_app_reduct Mapp H4) as [[MLabs NL] | [Napp Mred]]. left. exists MLabs. trivial. assert (appBodyL Mapp -b-> appBodyL Napp -> appBodyL Mapp >> appBodyL Napp). apply beta_imp_horpo. apply algebraic_appBodyL; try_solve. assert (appBodyR Mapp -b-> appBodyR Napp -> appBodyR Mapp >> appBodyR Napp). apply beta_imp_horpo. apply algebraic_appBodyR; try_solve. right; exists Napp; fo. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)