proposition: Lemma IH_horpoRC : forall L R, (subterm L M \/ (L = M /\ subterm R N)) -> {L >>= R} + {~L >>= R}.
proof: Proof. intros. destruct (@IH L R); trivial. left; left; trivial. destruct (eq_Term_dec L R). left; rewrite e; right. right; intro LR; inversion LR; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)