proposition: Lemma edge_func_spec: forall {pg : PreGraph V E} {lfg: LocalFiniteGraph pg} e x, In e (edge_func pg x) <-> evalid pg e /\ src pg e = x.
proof: Proof. intros. unfold edge_func. destruct (local_enumerable x) as [? [?H ?H]]; simpl. specialize (H0 e). rewrite H0; unfold out_edges. clear - H0. unfold Ensembles.In; tauto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas