proposition: Lemma Permutation_filter: forall A (L1 L2 : list A) (f : A -> bool), Permutation L1 L2 -> Permutation (filter f L1) (filter f L2).
proof: Proof. intros. induction H. constructor. simpl. case (f x). constructor. trivial. trivial. simpl. case (f x); case (f y). constructor. constructor. reflexivity. constructor. reflexivity. reflexivity. transitivity (filter f l'); 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