proposition: Lemma filter_false_nil: forall A (l: list A) f, (forall a, In a l -> f a = false) -> filter f l = [].
proof: Proof. intros. apply filter_empty. trivial. 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