proposition: Lemma step_dec: forall {pg : PreGraph V E} {lfg: LocalFiniteGraph pg} x y, {step pg x y} + {~step pg x y}.
proof: Proof. intros. destruct (in_dec EV y (map (dst pg) (edge_func pg x))). left. apply edge_func_step. trivial. right. intro. apply n. apply edge_func_step. trivial. 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