proposition: Lemma dp_step_equiv_aux_1 : forall r l , rdp_step (axiom (ddp R1)) R3 r l <-> rdp_step (axiom (ddp R2)) R3 r l.
proof: Proof. intros r l. split. inversion 1;subst. rewrite axiom_ddp_equiv in H1. constructor 1 with l2; assumption. inversion 1;subst. rewrite <- axiom_ddp_equiv in H1. constructor 1 with l2; assumption. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)