fact: Definition c_connected_by_path size (g: @EdgeListGG size) p u v := match u, v with | Vint u', Vint v' => connected_by_path g p (Int.signed u') (Int.signed v') | _, _ => False end.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist