proposition: Lemma horpo_var_normal : forall M N, isVar M -> ~(M >> N).
proof: Proof. intros M N Mvar MN. destruct MN. absurd (M >-> N); trivial. apply prehorpo_var_normal; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)