fact: Record BagPlusProof (TItem : Type) := { BagTypePlus : Type; SearchTermTypePlus : Type; UpdateTermTypePlus : Type; RepInvPlus : BagTypePlus -> Prop; ValidUpdatePlus : UpdateTermTypePlus -> Prop; BagPlus : Bag BagTypePlus TItem SearchTermTypePlus UpdateTermTypePlus; CorrectBagPlus : CorrectBag RepInvPlus ValidUpdatePlus BagPlus }.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Program.Program Coq.Sorting.Permutation