proposition: Lemma Empty_R_no_rdp_step : forall R x y, rdp_step (axiom (ddp Empty_R)) R x y -> False.
proof: Proof. intros. inversion H. inversion H1. destruct H6. apply Empty_R_no_dp with (1:=H6). Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)