val si_seq_length (#a #n: _) (il: interleaving a n)
    : Lemma (ensures (S.length il = S.length (si_seq il))) [SMTPat (si_seq il)]
val si_seq_length (#a #n: _) (il: interleaving a n)
    : Lemma (ensures (S.length il = S.length (si_seq il))) [SMTPat (si_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
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))
/
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
  -> FStar.Pervasives.Lemma
      (ensures FStar.Seq.Base.length il = FStar.Seq.Base.length (Zeta.MultiSet.SSeq.si_seq il))
      [SMTPat (Zeta.MultiSet.SSeq.si_seq il)]
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Zeta.Interleave.interleaving_flat_length FStar.Seq.Base.length FStar.Seq.Base.seq Prims.unit Prims.b2t Prims.op_Equality Zeta.SSeq.sseq Zeta.Interleave.s_seq Zeta.Interleave.some_interleaving Prims.l_True Prims.squash Zeta.Interleave.elem_src Zeta.MultiSet.SSeq.si_seq Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
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