proposition: Lemma rdp_step_equiv : forall r l, rdp_step (axiom (ddp R1)) R3 r l <-> rdp_step (axiom (ddp R2)) R4 r l.
proof: Proof. intros r l. transitivity (rdp_step (axiom (ddp R2)) R3 r l). apply dp_step_equiv_aux_1. apply dp_step_equiv_aux_2. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)