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