val tl (#a: eqtype) (#f: cmp a) (s: mset a f {Cons? s}) : mset a f
val tl (#a: eqtype) (#f: cmp a) (s: mset a f {Cons? s}) : mset a f
let tl (#a:eqtype) (#f:cmp a) (s:mset a f{Cons? s}) : mset a f = tl s
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


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)

let mset a f = l:list (a & pos){sorted f l}


/// We will use this function, rather than pattern matching to get better implicit inference
/
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
s: Zeta.MultiSet.mset a f {Cons? s} -> Zeta.MultiSet.mset a f
Prims.eqtype Zeta.MultiSet.cmp Zeta.MultiSet.mset Prims.b2t Prims.uu___is_Cons FStar.Pervasives.Native.tuple2 Prims.pos FStar.List.Tot.Base.tl
let tl (#a: eqtype) (#f: cmp a) (s: mset a f {Cons? s}) : mset a f =
  
tl s