fact: Definition bupdate_Preserves_RepInv {TContainer TItem TSearchTerm TUpdateTerm : Type} (RepInv : TContainer -> Prop) (ValidUpdate : TUpdateTerm -> Prop) (bupdate : TContainer -> TSearchTerm -> TUpdateTerm -> (list TItem) * TContainer) := forall container search_term update_term (containerCorrect : RepInv container) (valid_update : ValidUpdate update_term), RepInv (snd (bupdate container search_term update_term)).
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Program.Program Coq.Sorting.Permutation