proposition: Lemma NoDup_Perm_False: forall {A} {l1 l2: list A} {a}, NoDup l1 -> Permutation l1 (a :: a :: l2) -> False.
proof: Proof. intros. assert (NoDup (a :: a :: l2)). eapply Permutation_NoDup; eauto. inversion H1. apply H4. 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