val sorted (#a: eqtype) (f: cmp a) (l: list (a & pos)) : Type0
val sorted (#a: eqtype) (f: cmp a) (l: list (a & pos)) : Type0
let rec sorted (#a:eqtype) (f:cmp a) (l:list (a & pos)) : Type0 =
  match l with
  | [] -> True
  | [_] -> True
  | (x, _)::(y, card_y)::tl ->
    f x y /\
    x =!= y /\
    sorted f ((y, card_y)::tl)
module Zeta.MultiSet

open FStar.List.Tot


/// We represet a multiset with a sorted associative list
///   where the second component of each list element is the
///   cardinality of the first component in the set
///
/// The list is sorted on the first component of its elements
/
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Zeta.MultiSet.fst
f: Zeta.MultiSet.cmp a -> l: Prims.list (a * Prims.pos) -> Type0
Prims.eqtype Zeta.MultiSet.cmp Prims.list FStar.Pervasives.Native.tuple2 Prims.pos Prims.l_True Prims.l_and Prims.b2t Prims.l_not Prims.eq2 Zeta.MultiSet.sorted Prims.Cons FStar.Pervasives.Native.Mktuple2
let rec sorted (#a: eqtype) (f: cmp a) (l: list (a & pos)) : Type0 =
  
match l with
| [] -> True
| [_] -> True
| (x, _) :: (y, card_y) :: tl -> f x y /\ x =!= y /\ sorted f ((y, card_y) :: tl)