proposition: Lemma Permutation_Zlength: forall A (L1 : list A) L2, Permutation L1 L2 -> Zlength L1 = Zlength L2.
proof: Proof. intros. apply Permutation_length in H. do 2 rewrite Zlength_correct. congruence. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model