proposition: Lemma dp_equiv_empty_pi : forall (R:relation term) pi v1 v2 (Hpi:is_primary_pi pi R) x y, dp (union _ (union _ R Empty_R) (Pi pi v1 v2)) x y <-> dp R x y.
proof: Proof. intros R pi v1 v2 Hpi x y. rewrite pi_no_dp. apply dp_equiv; clear. intros l r. apply Empty_R_neutral_union_l. intros s t H f. inversion_clear H. apply Hpi; exact H0. inversion H0. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)