proposition: Lemma valid_parent: forall (g: UFGraph) v n p, vvalid g v -> vgamma g v = (n, p) -> vvalid g p.
proof: Proof. intros. unfold vgamma in H0. simpl in H0. inversion H0. clear H0 H2. destruct (projT2 isNullDec (dst g (out_edge v))); auto. assert (~ isNullDec (dst g (out_edge v))) by (intro; apply n0; auto). pose proof (only_one_edge v (out_edge v) H). assert (out_edge v = out_edge v) by auto. rewrite <- H1 in H2. destruct H2. pose proof (valid_graph _ _ H4). destruct H5 as [_ [? | ?]]; auto. exfalso; 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