val indefinite_description_two (#a #b: Type) (p: (a -> b -> ubool))
    : Ghost (a * b)
      (requires exists x y. p x y)
      (ensures
        fun xy ->
          let x, y = xy in
          p x y)
val indefinite_description_two (#a #b: Type) (p: (a -> b -> ubool))
    : Ghost (a * b)
      (requires exists x y. p x y)
      (ensures
        fun xy ->
          let x, y = xy in
          p x y)
let indefinite_description_two (#a: Type) (#b: Type) (p: (a -> b -> ubool)) : Ghost (a * b)
  (requires exists x y. p x y)
  (ensures  fun xy -> let x, y = xy in p x y) =
  let p': (a * b) -> prop = fun xy -> squash (let x, y = xy in p x y) in
  eliminate exists x' y'. p x' y'
  returns exists xy. p' xy
  with _. (assert (let x, y = (x', y') in p x y));
  FStar.IndefiniteDescription.indefinite_description_ghost (a * b) p'
module Util.Logic

open Spec.Logic
open Spec.Ubool

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'
/
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 -> _: b -> Spec.Ubool.ubool) -> Prims.Ghost (a * b)
Spec.Ubool.ubool FStar.IndefiniteDescription.indefinite_description_ghost FStar.Pervasives.Native.tuple2 Prims.unit FStar.Classical.Sugar.exists_elim Prims.l_Exists Prims.squash Prims._assert FStar.Pervasives.Native.Mktuple2 Prims.prop
let indefinite_description_two (#a #b: Type) (p: (a -> b -> ubool))
    : Ghost (a * b)
      (requires exists x y. p x y)
      (ensures
        fun xy ->
          let x, y = xy in
          p x y) =
  
let p': (a * b) -> prop =
  fun xy ->
    squash (let x, y = xy in
        p x y)
in
eliminate exists x' y'.
p x' y'
returns exists xy. p' xy
with _.
(assert (let x, y = (x', y') in
      p x y));
FStar.IndefiniteDescription.indefinite_description_ghost (a * b) p'