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