proposition: Lemma filter_map_comm: forall A B (f : A -> bool) (g : B -> bool) (h : A -> B) (L : list A), (forall x, f x = g (h x)) -> filter g (map h L) = map h (filter f L).
proof: Proof. induction L; intros. reflexivity. simpl. rewrite <- H. case (f a); auto. simpl. f_equal. auto. 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