proposition: Lemma compute_neighbor: forall x l, vvalid G x -> reachable_list G x l -> forall y, step G x y -> {l' | reachable_list G y l' /\ NoDup l'}.
proof: Proof. intros. pose proof valid_step _ _ _ H1. destruct (@null_or_valid _ _ _ _ _ G _ _ (proj2 H2)). + subst. exists nil. split. - intro. split; intro; [inversion H3 |]. apply reachable_head_valid in H3. apply (@valid_not_null _ _ _ _ G is_null) in H3; auto. - apply NoDup_nil. + apply (compute_reachable x l). - auto. - apply reachable_edge with x. 1: apply reachable_refl; auto. hnf. auto. Qed.
imports: Coq.Sets.Finite_sets Coq.Arith.Arith Coq.Logic.ProofIrrelevance Coq.Logic.FunctionalExtensionality Coq.Sorting.Permutation Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles Coq.Lists.List VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph