proposition: Lemma NatIPool_pfresh_correct : forall pool, NatIPool_pget pool (NatIPool_pfresh pool) = None.
proof: Proof. unfold NatIPool_pget, NatIPool_pfresh; intros [ [m n] pf]; simpl. destruct (find (elt:=TItem) n m) eqn: eq; eauto. apply find_2 in eq. apply pf in eq. simpl in eq. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.Structures.OrderedTypeEx