proposition: Lemma edge_func_step: forall {pg : PreGraph V E} {lfg: LocalFiniteGraph pg} x y, step pg x y <-> In y (map (dst pg) (edge_func pg x)).
proof: Proof. intros. rewrite step_spec. rewrite in_map_iff. apply Morphisms_Prop.ex_iff_morphism. hnf; cbv beta; intro e. rewrite edge_func_spec. clear - e. 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