proposition: Lemma R_var_empty : forall (l r : term), In (l,r) nil -> forall v, l <> Var v.
proof: Proof. intros l r H; case H. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)