val gen_seq : vspec: Zeta.GenericVerifier.verifier_spec -> n: Prims.nat -> Zeta.IdxFn.gen_seq_spec
let gen_seq (vspec:verifier_spec) (n:_) = {
  IF.a = I.elem_src (verifier_log_entry vspec) n;
  IF.phi = verifiable;
  IF.phi_commutes_with_prefix = (fun il i -> lemma_prefix_verifiable n il i);
}
module Zeta.Generic.Blum

open Zeta.Ghost
open Zeta.SMap
open FStar.Classical

module IF = Zeta.IdxFn
module T = Zeta.Generic.Thread
/
Zeta.SMap.fsti.checked Zeta.MultiSet.SSeq.fsti.checked Zeta.IdxFn.fsti.checked Zeta.Ghost.fsti.checked Zeta.Generic.Thread.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Generic.Blum.fst
vspec: Zeta.GenericVerifier.verifier_spec -> n: Prims.nat -> Zeta.IdxFn.gen_seq_spec
Zeta.GenericVerifier.verifier_spec Prims.nat Zeta.IdxFn.Mkgen_seq_spec Zeta.Interleave.elem_src Zeta.GenericVerifier.verifier_log_entry Zeta.Generic.Interleave.verifiable FStar.Seq.Base.seq Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Zeta.Generic.Interleave.lemma_prefix_verifiable Prims.unit Zeta.IdxFn.gen_seq_spec
let gen_seq (vspec: verifier_spec) (n: _) =
  
{
  IF.a = I.elem_src (verifier_log_entry vspec) n;
  IF.phi = verifiable;
  IF.phi_commutes_with_prefix = (fun il i -> lemma_prefix_verifiable n il i)
}