proposition: Lemma IndexedBag_BagInsertEnumerate : BagInsertEnumerate IndexedBag_RepInv IndexedBag_benumerate IndexedBag_binsert.
proof: Proof. unfold IndexedBag_benumerate, IndexedBag_RepInv, IndexedBag_binsert. hnf; simpl; intros ins bag [repi repp]. eapply perm_trans; [ eapply IndexesToItems_perm; try eapply ibinsert_enumerate | ]; eauto. simpl; rewrite pput_eq; constructor. remember (ibenumerate (fst bag)) as ls; clear Heqls. pose proof (fun idx => proj1 (repp idx)) as repp_f; clear repp. induction ls; simpl; eauto. destruct (InList_ind_helper repp_f) as [repp_f_h repp_f_t]; clear repp_f. rewrite pput_neq; eauto. destruct (pget (snd bag) a); eauto. intro contra; subst; apply repp_f_h; apply pfresh_correct. 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