proposition: Lemma step_spec: forall (pg: PreGraph Vertex Edge) x y, step pg x y <-> exists e, evalid pg e /\ src pg e = x /\ dst pg e = y.
proof: Proof. intros; split; intro. + inversion H; eauto. + destruct H as [? [? [? ?]]]; econstructor; eauto. 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