proposition: Lemma Empty_R_no_dp : forall x y, dp Empty_R x y -> False.
proof: Proof. intros. inversion H. inversion H0. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)