proposition: Lemma Permutation_Zlength: forall {A: Type} (l l': list A), Permutation l l' -> Zlength l = Zlength l'.
proof: Proof. intros. assert (length l = length l'). apply Permutation_length. apply H. repeat rewrite Zlength_correct. rewrite H0. auto. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver