proposition: Lemma NatIPool_pput_eq : forall pool idx item, NatIPool_pget (NatIPool_pput pool idx item) idx = item.
proof: Proof. unfold NatIPool_pget, NatIPool_pput. intros [ [m n] pf] idx item; destruct item eqn: eq; simpl; subst. - eapply add_eq_o; eauto. - eapply remove_eq_o; eauto. 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