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