fact: Variable R_app_reduct : forall M N (Mapp: isApp M), ~isFunApp M \/ isArrowType (type M) -> M -R-> N -> (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 -R-> appBodyR Napp) \/ (appBodyL Mapp -R-> appBodyL Napp /\ appBodyR Mapp = appBodyR Napp) \/ (appBodyL Mapp -R-> appBodyL Napp /\ appBodyR Mapp -R-> appBodyR Napp).
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)