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