val sseq2mset (#a:eqtype) (#f:cmp a) (s:sseq a) : mset a f
val sseq2mset (#a:eqtype) (#f:cmp a) (s:sseq a) : mset a f
let sseq2mset (#a:eqtype) (#f:cmp a) (s:sseq a) : mset a f
  = let open Zeta.Interleave in
    let il = some_interleaving s in
    seq2mset (i_seq il)
module Zeta.MultiSet.SSeq

open FStar.Classical
/
Zeta.SSeq.fsti.checked Zeta.SeqAux.fsti.checked Zeta.MultiSet.fsti.checked Zeta.Interleave.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Zeta.MultiSet.SSeq.fst
s: Zeta.SSeq.sseq a -> Zeta.MultiSet.mset a f
Prims.eqtype Zeta.MultiSet.cmp Zeta.SSeq.sseq Zeta.MultiSet.seq2mset Zeta.Interleave.i_seq FStar.Seq.Base.length FStar.Seq.Base.seq Zeta.Interleave.interleaving Prims.b2t Prims.op_Equality Zeta.Interleave.s_seq Zeta.Interleave.some_interleaving Zeta.MultiSet.mset
let sseq2mset (#a: eqtype) (#f: cmp a) (s: sseq a) : mset a f =
  
let open Zeta.Interleave in
let il = some_interleaving s in
seq2mset (i_seq il)