proposition: Lemma module_Empty_R : module R1 Empty_R.
proof: Proof. constructor. intros f2 s t def_f2 s_t. inversion def_f2;subst. inversion H. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)