proposition: Lemma vertex_prop_coincide_sym: forall (g1 g2: PreGraph Vertex Edge) (p1 p2: Vertex -> Prop), vertex_prop_coincide g1 g2 p1 p2 -> vertex_prop_coincide g2 g1 p2 p1.
proof: Proof. unfold vertex_prop_coincide. intros. symmetry. auto. 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