proposition: Lemma parent_loop: forall (g: UFGraph) v n y, vgamma g v = (n, v) -> reachable g v y -> v = y.
proof: Proof. intros. unfold vgamma in H. destruct (projT2 isNullDec (dst g (out_edge v))). - apply (lst_out_edge_only_one g _ v (dst g (out_edge v)) y); auto. intro. apply reachable_head_valid in H1. apply (valid_not_null g (dst g (out_edge v)) H1); auto. - apply (lst_self_loop _ (liGraph g)) in H0; auto. inversion H. rewrite H3. auto. Qed.
imports: Coq.Sets.Ensembles Coq.Lists.List CertiGraph.lib.EquivDec_ext CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.UnionFind