proposition: Lemma vertex_prop_coincide_refl: forall (g: PreGraph Vertex Edge) (p: Vertex -> Prop), vertex_prop_coincide g g p p.
proof: Proof. intros. hnf; intros. reflexivity. 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