proposition: Lemma prehorpo_var_normal : forall N M, isVar M -> ~ (M >-> N).
proof: Proof. intro N. apply well_founded_ind with (R := subterm) (P := fun N => forall M, isVar M -> ~(M >-> N)). apply subterm_wf. clear N; intros N IH M Mvar MN. induction MN; term_inv M. inversion H; inversion H0; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)