val i2si (#a #n: _) (il: interleaving a n) (i: SA.seq_index il)
    : j: SA.seq_index (si_seq il) {S.index (i_seq il) i = S.index (si_seq il) j}
val i2si (#a #n: _) (il: interleaving a n) (i: SA.seq_index il)
    : j: SA.seq_index (si_seq il) {S.index (i_seq il) i = S.index (si_seq il) j}
let i2si (#a #n:_) (il: interleaving a n) (i: SA.seq_index il)
  : j:SA.seq_index (si_seq il){S.index (i_seq il) i = S.index (si_seq il) j}
  = let is = i_seq il in
    let ss = s_seq il in
    let il2 = some_interleaving ss in
    let ii = i2s_map il i in
    s2i_map il2 ii
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)

let si_seq (#a #n:_) (il: interleaving a n)
  = i_seq (some_interleaving (s_seq il))

let si_seq_length (#a #n:_) (il: interleaving a n)
  : Lemma (ensures (S.length il = S.length (si_seq il)))
          [SMTPat (si_seq il)]
  = let ss = s_seq il in
    let il2 = some_interleaving ss in
    interleaving_flat_length il;
    interleaving_flat_length il2
/
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 -> i: Zeta.SeqAux.seq_index il
  -> j:
    Zeta.SeqAux.seq_index (Zeta.MultiSet.SSeq.si_seq il)
      { FStar.Seq.Base.index (Zeta.Interleave.i_seq il) i =
        FStar.Seq.Base.index (Zeta.MultiSet.SSeq.si_seq il) j }
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Zeta.SeqAux.seq_index Zeta.Interleave.elem_src Zeta.Interleave.s2i_map FStar.Seq.Base.length FStar.Seq.Base.seq Zeta.SSeq.sseq_index Zeta.Interleave.s_seq Prims.l_and Prims.b2t Prims.op_Equality Zeta.Interleave.index Zeta.SSeq.indexss FStar.Pervasives.Native.fst Zeta.Interleave.src Zeta.Interleave.i2s_map Zeta.SSeq.sseq Zeta.Interleave.some_interleaving Zeta.Interleave.i_seq Zeta.MultiSet.SSeq.si_seq FStar.Seq.Base.index
let i2si (#a #n: _) (il: interleaving a n) (i: SA.seq_index il)
    : j: SA.seq_index (si_seq il) {S.index (i_seq il) i = S.index (si_seq il) j} =
  
let is = i_seq il in
let ss = s_seq il in
let il2 = some_interleaving ss in
let ii = i2s_map il i in
s2i_map il2 ii