proposition: Lemma valid_path_find_list: forall bound v l, vvalid g v -> pfoot' g (rev l) v = v -> valid_path' g (rev l) -> valid_path g (edge_list_head (rev l) v, find_list bound v l).
proof: Proof. intros. simpl. destruct (find_list_foreside bound v l) as [l' ?]. destruct (find_list bound v l) eqn:? . - symmetry in H2. apply app_eq_nil in H2. destruct H2. rewrite H2. simpl; auto. - split. 2: rewrite <- Heql0; apply valid_path'_find_list; auto. destruct l. + simpl in *. destruct bound; simpl in Heql0. * destruct (projT2 is_null (dst g (out_edge v))); inversion Heql0. * destruct (projT2 is_null (dst g (out_edge v))). 1: inversion Heql0. destruct (find_list_foreside bound (dst g (out_edge v)) (out_edge v :: nil)) as [l'' ?]. rewrite Heql0 in H3. simpl in H3. inversion H3. pose proof (vvalid_src_evalid g gLst v H). destruct H4; auto. + remember (rev (e0 :: l)) eqn:? . destruct l1. 1: exfalso; simpl in Heql1; destruct (rev l); inversion Heql1. simpl in *. inversion H2. auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext CertiGraph.lib.EnumEnsembles CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable