proposition: Lemma toEdgeList_unfold: forall i, toEdgeList i = match i with (len, x, r) => if Compare_dec.le_dec len (length r) then r else let eList := filterE (edge_func g x) in match eList with | nil => r | e :: _ => toEdgeList (len, dst g e, (e, dst g e) :: r) end end.
proof: Proof. intros. destruct i as [[len x] r]. unfold toEdgeList at 1. rewrite Fix_eq. + destruct (Compare_dec.le_dec len (length r)); auto. + intros. assert (f = g0) by (extensionality y; extensionality p; auto). subst; auto. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph