proposition: Lemma Rvar' : forall x t, ~ (In (Var x,t) rule_list).
proof: Proof. intros t x H; apply (Rvar x t); rewrite Req; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)