proposition: Lemma prehorpo_dec : forall M N, (forall L R, (subterm L M \/ (L = M /\ subterm R N)) -> {L >> R} + {~L >> R}) -> env M = env N -> type M = type N -> algebraic M -> algebraic N -> {M >-> N} + {~ M >-> N}.
proof: Proof. intros M N IH MNenv MNtype Malg Nalg. assert (IHeq: forall L R, (subterm L M \/ (L = M /\ subterm R N)) -> {L >>= R} + {~L >>= R} ). intros. destruct (IH L R); trivial. left; constructor; trivial. destruct (eq_Term_dec L R). rewrite e; left; constructor 2. right; intro LR; destruct LR; auto. destruct (beta_dec M N). left. apply HBeta. hyp. destruct (isFunApp_dec M). destruct (@HSub_dec M N); trivial. left; apply HSub; trivial. destruct (@HAppFlat_dec M N); trivial. destruct s as [Ns NsN MNs]. left; apply HAppFlat with Ns; trivial. destruct (@HMul_dec M N); trivial. destruct s as [f [Mf [Nf MNargs]]]. left; apply HMul with f; trivial. destruct (@HFun_dec M N); trivial. destruct s as [[f g] [Mf [Ng [fg MNargs]]]]. left; apply HFun with f g; trivial. right; intro MN; inversion MN; try_solve. destruct o0 as [Nnfa | [abs | MargsN]]; try_solve. absurd (isFunApp N); trivial. unfold isFunApp; apply funS_is_funS with g; trivial. absurd (f >#> g); auto. destruct o; try_solve. apply n1; exists Ns; trivial. term_inv M. destruct (term_case M) as [[[Mvar | Mfuns] | Mabs] | Mapp]. right. apply prehorpo_var_normal; simpl; trivial. absurd (isFunApp M); trivial. term_inv M. destruct (isAbs_dec N) as [Nabs | Nnabs]. destruct (IH (absBody Mabs) (absBody Nabs)). left; apply absBody_subterm. left; apply HAbs with Mabs Nabs; trivial. right; intro TrN. inversion TrN; term_inv M. apply n1; trivial. rewrite (abs_proof_irr N Nabs NAbs); trivial. right; intro TrN. inversion TrN; term_inv M. assert (forall f, term (appHead M) = ^f -> False). intros; apply n0; unfold isFunApp. apply funS_is_funS with f; trivial. destruct (isApp_dec N) as [Napp | Nnapp]. destruct (isFunApp_dec N) as [Nfapp | Nnfapp]. right. intro MN. inversion MN; try solve [term_inv M; apply H with f; trivial]. destruct (IHeq (appBodyL Mapp) (appBodyL Napp)). left; apply appBodyL_subterm. destruct (IHeq (appBodyR Mapp) (appBodyR Napp)). left; apply appBodyR_subterm. destruct (IH (appBodyL Mapp) (appBodyL Napp)). left; apply appBodyL_subterm. left; apply HApp with Mapp Napp; trivial. constructor; apply pair_mOrd_left; trivial. apply horpo_eq_compat'. destruct h0; [left | right]; auto with sets. destruct (IH (appBodyR Mapp) (appBodyR Napp)). left; apply appBodyR_subterm. left; apply HApp with Mapp Napp; trivial. constructor; apply pair_mOrd_right; trivial. apply horpo_eq_compat'. destruct h; [left | right]; auto with sets. right; intro TrN. inversion TrN; try solve [term_inv M; apply H with f; trivial]. destruct (horpo_app M N MApp NApp MNtype) as [_ [_ [LL | RR]]]; trivial. apply n1; trivial. rewrite (app_proof_irr M Mapp MApp), (app_proof_irr N Napp NApp); trivial. apply n2; trivial. rewrite (app_proof_irr M Mapp MApp), (app_proof_irr N Napp NApp); trivial. right; intro TrN. inversion TrN; try solve [term_inv M; apply H with f; trivial]. destruct (horpo_app M N MApp NApp MNtype) as [_ [RR _]]; trivial. apply n1. rewrite (app_proof_irr M Mapp MApp), (app_proof_irr N Napp NApp); trivial. right; intro TrN. inversion TrN; try solve [term_inv M; apply H with f; trivial]. destruct (horpo_app M N MApp NApp MNtype) as [LL [_ _]]; trivial. apply n1. rewrite (app_proof_irr M Mapp MApp), (app_proof_irr N Napp NApp); trivial. right; intro TrN. inversion TrN; try solve [term_inv M; apply H with f; trivial]. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)