proposition: Lemma horpo_app : forall M N (Mapp: isApp M) (Napp: isApp N), type M = type N -> {{appBodyL Mapp, appBodyR Mapp}} {>>} {{appBodyL Napp, appBodyR Napp}} -> appBodyL Mapp >>= appBodyL Napp /\ appBodyR Mapp >>= appBodyR Napp /\ (appBodyL Mapp >> appBodyL Napp \/ appBodyR Mapp >> appBodyR Napp).
proof: Proof. assert (Htyp: forall M N, M >> N \/ M = N -> type M = type N). intros. destruct H. apply horpo_type_preserving; trivial. rewrite H; trivial. intros. inversion H0. term_inv M; term_inv N. try (rename A0 into A1; rename A into A0). destruct (pair_mOrd horpo_eq_compat' H1) as [o1 | [o2 | [o3 | o4]]]. absurd (A1 = A1 --> B0). apply type_discr. replace (A1 --> B0) with (A0 --> B). replace A1 with (A0 --> B); trivial. fold (type (buildT T1)). fold (type (buildT T4)). apply Htyp; try_solve. fold (type (buildT T1)). fold (type (buildT T3)). apply Htyp; try_solve. absurd (A1 = A1 --> B0). apply type_discr. replace (A1 --> B0) with A0. replace A1 with A0; trivial. fold (type (buildT T2)). fold (type (buildT T4)). apply Htyp; try_solve. fold (type (buildT T2)). fold (type (buildT T3)). apply Htyp; try_solve. destruct o3 as [c1 [c2 c3]]. repeat split. destruct c1. left; trivial. unfold eqA in H4; unfold TermsEqset.eqA in H4. rewrite H4; right. destruct c2. left; trivial. unfold eqA in H4; unfold TermsEqset.eqA in H4. rewrite H4; right. destruct c3; try_solve. absurd (A0 = (A0 --> B) --> B0). apply type_discr2. replace (A0 --> B) with A1. fold (type (buildT T2)). fold (type (buildT T3)). apply Htyp; try_solve. fold (type (buildT T1)). fold (type (buildT T4)). sym. apply Htyp; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)