proposition: Lemma filter_empty: forall A f (L : list A), (forall x, In x L -> f x = false) -> filter f L = [].
proof: Proof. induction L; intros. reflexivity. simpl. rewrite H. apply IHL. intros. apply H. right. trivial. left. 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