val u2b (u: ubool) : GTot bool
val u2b (u: ubool) : GTot bool
let u2b (u: ubool) : GTot bool =
  FStar.IndefiniteDescription.strong_excluded_middle u
module Spec.Ubool

type ubool = Type0 // not-necessarily-decidable boolean
/
prims.fst.checked FStar.Pervasives.fsti.checked FStar.IndefiniteDescription.fsti.checked
Spec.Ubool.fst
u2: Spec.Ubool.ubool -> Prims.GTot Prims.bool
Spec.Ubool.ubool FStar.IndefiniteDescription.strong_excluded_middle Prims.bool
let u2b (u: ubool) : GTot bool =
  
FStar.IndefiniteDescription.strong_excluded_middle u