val exists_elems_with_prop : p: (_: a -> Prims.bool) -> s: FStar.Seq.Base.seq a -> Prims.logical
let exists_elems_with_prop (#a:_) (p: a -> bool) (s: seq a)
  = exists i. p (index s i)
module Zeta.SeqIdx

open FStar.Seq
open Zeta.SeqAux
/
Zeta.SeqAux.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.SeqIdx.fsti
p: (_: a -> Prims.bool) -> s: FStar.Seq.Base.seq a -> Prims.logical
Prims.bool FStar.Seq.Base.seq Prims.l_Exists Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length FStar.Seq.Base.index Prims.logical
let exists_elems_with_prop (#a: _) (p: (a -> bool)) (s: seq a) =
  
exists i. p (index s i)