proposition: Lemma keys_valid_tl: forall hi h, keys_valid (hi :: h) -> keys_valid h.
proof: Proof. intros. eapply List_ext.NoDup_cons_1, H. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel