fact: Definition BagInsertEnumerate {TContainer TItem: Type} (RepInv : TContainer -> Prop) (benumerate : TContainer -> list TItem) (binsert : TContainer -> TItem -> TContainer) := forall inserted container (containerCorrect : RepInv container), Permutation (benumerate (binsert container inserted)) (inserted :: benumerate container).
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Program.Program Coq.Sorting.Permutation