proposition: Lemma axiom_ddp_equiv : forall l r, axiom (ddp R1) r l <-> axiom (ddp R2) r l.
proof: Proof. split. inversion 1. destruct H0 as [H0 Sub]. rewrite dp_equiv in H0. constructor; split; assumption. inversion 1. destruct H0 as [H0 Sub]. rewrite <- dp_equiv in H0. constructor; split; assumption. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)