val simpler_indefinite_description (#a: Type) ($p: (a -> ubool))
    : Ghost a (requires exists x. p x) (ensures fun x -> p x)
val simpler_indefinite_description (#a: Type) ($p: (a -> ubool))
    : Ghost a (requires exists x. p x) (ensures fun x -> p x)
let simpler_indefinite_description (#a: Type) ($p: a -> ubool) : Ghost a
  (requires exists x. p x)
  (ensures  fun x -> p x) =
  let p': a -> prop = fun x -> squash (p x) in
  FStar.IndefiniteDescription.indefinite_description_ghost a p'
module Util.Logic

open Spec.Logic
open Spec.Ubool
/
Spec.Ubool.fst.checked Spec.Logic.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.IndefiniteDescription.fsti.checked FStar.Classical.Sugar.fsti.checked
Util.Logic.fst
$p: (_: a -> Spec.Ubool.ubool) -> Prims.Ghost a
Spec.Ubool.ubool FStar.IndefiniteDescription.indefinite_description_ghost Prims.prop Prims.squash Prims.l_Exists
let simpler_indefinite_description (#a: Type) ($p: (a -> ubool))
    : Ghost a (requires exists x. p x) (ensures fun x -> p x) =
  
let p': a -> prop = fun x -> squash (p x) in
FStar.IndefiniteDescription.indefinite_description_ghost a p'