proposition: Lemma rdp_equiv_empty_l : forall (R R':relation term) x y, rdp_step (axiom (ddp (union _ R Empty_R))) R' x y <-> rdp_step (axiom (ddp R)) R' x y.
proof: Proof. intros R R' x y. apply rdp_step_equiv_strong. clear;intros;apply dp_equiv. clear; intros l r;apply Empty_R_neutral_union_l. reflexivity. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)