proposition: Lemma uf_root_not_eq_root_vgamma: forall (g: UFGraph) x r pa root, vgamma g x = (r, pa) -> uf_root g x root -> x <> root -> x <> pa.
proof: Proof. intros. unfold vgamma in H. destruct (projT2 isNullDec (dst g (out_edge x))). - destruct H0. apply reachable_ind.reachable_ind in H0. destruct H0. 1: exfalso; auto. destruct H0 as [z [[? [? ?]] [? ?]]]. rewrite step_spec in H4. destruct H4 as [ed [? [? ?]]]. pose proof (conj H7 H4). rewrite (@only_one_edge _ _ _ _ g _ (liGraph g)) in H9; auto. subst ed. rewrite H8 in p. exfalso. apply (@valid_not_null _ _ _ _ g _ (maGraph g)) in H3; auto. - inversion H. clear H H3. assert (vvalid g x) by (destruct H0; apply reachable_head_valid in H; auto). assert (g |= (x, (out_edge x) :: nil) is x ~o~> pa satisfying (fun _ => True)). { split; split; intros; hnf; simpl; auto. unfold strong_evalid. assert (out_edge x = out_edge x) by auto. rewrite <- (@only_one_edge _ _ _ _ g _ (liGraph g)) in H2; auto. destruct H2. split; [|split]; auto. rewrite H2. split; auto. apply (@valid_graph _ _ _ _ g _ (maGraph g)) in H3. destruct H3 as [_ [? | ?]]; auto. hnf in H3. exfalso; auto. } rewrite H4. intro. rewrite <- H3 in H2. apply (@no_loop_path _ _ _ _ g _ (liGraph g)) in H2. inversion H2. 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