proposition: Lemma pi_no_dp : forall (R:relation term) pi v1 v2 (Hpi:is_primary_pi pi R) x y, dp (union _ R (Pi pi v1 v2)) x y <-> dp R x y.
proof: Proof. intros R pi v1 v2 Hpi x y. split. intros H. inversion H;clear H;subst. inversion H0;clear H0. constructor 1 with t2 p;auto. inversion H2; subst. inversion H0; clear H0. constructor 1 with l t; exact H3. inversion H3; subst f2; subst; clear H3. apply False_ind. eapply is_primary_pi_not_subrule; try eassumption. apply False_ind. eapply is_primary_pi_not_subrule; try eassumption. inversion H;clear H;subst. destruct p;simpl in H2;discriminate. destruct p;simpl in H2;discriminate. intro H. inversion H;clear H;subst. constructor 1 with t2 p;trivial. left;exact H0. inversion H2; subst f2; subst. constructor 1 with l t. left; exact H. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)