proposition: Lemma Rreg' : (forall l r, In (l,r) rule_list -> forall x, In x (var_list r) -> In x (var_list l)).
proof: Proof. intros l r H. apply Rreg; rewrite Req; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)