val si_seq : il: Zeta.Interleave.interleaving a n
  -> is:
    FStar.Seq.Base.seq a
      { FStar.Seq.Base.length is =
        FStar.Seq.Base.length (Zeta.Interleave.some_interleaving (Zeta.Interleave.s_seq il)) }
let si_seq (#a #n:_) (il: interleaving a n)
  = i_seq (some_interleaving (s_seq il))
module Zeta.MultiSet.SSeq

open FStar.Classical

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)
/
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
il: Zeta.Interleave.interleaving a n
  -> is:
    FStar.Seq.Base.seq a
      { FStar.Seq.Base.length is =
        FStar.Seq.Base.length (Zeta.Interleave.some_interleaving (Zeta.Interleave.s_seq il)) }
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Zeta.Interleave.i_seq FStar.Seq.Base.length FStar.Seq.Base.seq Zeta.Interleave.s_seq Zeta.Interleave.some_interleaving Prims.b2t Prims.op_Equality Zeta.Interleave.elem_src
let si_seq (#a #n: _) (il: interleaving a n) =
  
i_seq (some_interleaving (s_seq il))