proposition: Lemma dp_equiv : forall l r, dp R1 r l <-> dp R2 r l.
proof: Proof. split. inversion 1. rewrite R1_equiv_R2 in H0. econstructor; try eassumption. rewrite defined_equiv in H2;exact H2. inversion 1. rewrite <- R1_equiv_R2 in H0. econstructor; try eassumption. rewrite <- defined_equiv in H2;exact H2. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)