proposition: Lemma Perm_Perm_cons_Perm: forall {A} {l1 l2 l3: list A} {a b}, Permutation l1 (a :: l2) -> Permutation l2 (b :: l3) -> Permutation l1 (a :: b :: l3).
proof: Proof. intros. transitivity (a :: l2). trivial. constructor. 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