proposition: Lemma negateP_spec': forall (p : NodePred Vertex), Same_set (negateP p) (Complement _ p).
proof: Proof. intros. rewrite Same_set_spec; intros ?. apply negateP_spec. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext