proposition: Lemma module_empty : forall R, module Empty_R R.
proof: Proof. intros R; apply Mod. intros f s t _ H; case H. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)