proposition: Lemma horpo_dec: forall M N, {M >> N} + {~ M >> N}.
proof: Proof. intros M N. assert (Res: forall P, {fst P >> snd P} + {~fst P >> snd P}). intro P. apply well_founded_induction_type with (R := LexProd_Lt) (P := fun P => {fst P >> snd P} + {~fst P >> snd P}). apply lexprod_wf. unfold ltL, gtR, subterm_gt. rewrite transp_invol. apply subterm_wf. unfold ltR, gtR, subterm_gt. rewrite transp_invol. apply subterm_wf. clear M N P. intros P. destruct P as [M N]; simpl; intro IH. destruct (eq_SimpleType_dec (type M) (type N)). destruct (eq_Env_dec (env M) (env N)). destruct (algebraic_dec M). destruct (algebraic_dec N). destruct (@prehorpo_dec M N); trivial. intros. destruct (IH (L, R)). destruct H. left; trivial. right; destruct H; simpl; trivial. rewrite H; auto with sets. left; trivial. right; trivial. left; constructor; trivial. right; intro MN; inversion MN; try_solve. right; intro MN; inversion MN; try_solve. right; intro MN; inversion MN; try_solve. right; intro MN; inversion MN; try_solve. right; intro MN; inversion MN; try_solve. destruct (Res (M, N)); auto. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)