proposition: Lemma graph_same_size: forall (g g': UFGraph) n n', (forall x : Z, vvalid g x <-> vvalid g' x) -> (forall v : Z, 0 <= v < Z.of_nat n' <-> vvalid (lg_gg g') v) -> (forall v : Z, 0 <= v < Z.of_nat n <-> vvalid (lg_gg g) v) -> n = n'.
proof: Proof. intros. assert (forall v, 0 <= v < Z.of_nat n' <-> 0 <= v < Z.of_nat n). intros. rewrite H0. rewrite H1. symmetry. apply H. clear -H2. destruct (lt_eq_lt_dec n n'); [destruct s|]; auto; exfalso. - specialize (H2 (Z.of_nat n)). lia. - specialize (H2 (Z.of_nat n')). lia. Qed.
imports: CertiGraph.lib.List_ext CertiGraph.unionfind.env_unionfind_arr CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.graph.UnionFind CertiGraph.msl_application.ArrayGraph CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_array_graph Coq.Lists.List CertiGraph.unionfind.uf_arr_specs VST.floyd.library