proposition: Lemma horpo_app_inv : forall M N (Mapp: isApp M) (Napp: isApp N), ~isFunApp M -> algebraic M -> ~isFunApp N -> algebraic N -> appBodyL Mapp >>= appBodyL Napp /\ appBodyR Mapp >>= appBodyR Napp /\ (appBodyL Mapp >> appBodyL Napp \/ appBodyR Mapp >> appBodyR Napp) -> M >> N.
proof: Proof. intros. destruct H3 as [Leq [Req LRgt]]. constructor; trivial. apply app_type_eq with Mapp Napp; trivial. apply horpo_RC_type_preserving. hyp. apply horpo_RC_type_preserving. hyp. rewrite <- appBodyL_env with M Mapp, <- appBodyL_env with N Napp. apply horpo_RC_env_preserving. hyp. apply HApp with Mapp Napp; trivial. constructor. destruct LRgt. apply pair_mOrd_left; try_solve. inversion Req; intuition. apply pair_mOrd_right; try_solve. inversion Leq; intuition. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)