proposition: Lemma rank_unchanged_in_bound: forall (g g': UFGraph), uf_equiv g g' -> rank_unchanged g g' -> vlabel_in_bound g -> vlabel_in_bound g'.
proof: Proof. unfold uf_equiv, rank_unchanged, vlabel_in_bound. intros. destruct H as [? _]. pose proof H2. rewrite <- H in H2. rewrite <- H0; auto. Qed.
imports: CertiGraph.unionfind.env_unionfind CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.GList CertiGraph.msl_application.GList_UnionFind CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_graph_glist