val neqb : x: a -> y: a -> Prims.GTot Prims.bool
let neqb (#a: Type) (x: a) (y: a) =
  not (eqb x y)
module Spec.Ubool

type ubool = Type0 // not-necessarily-decidable boolean

let u2b (u: ubool) : GTot bool =
  FStar.IndefiniteDescription.strong_excluded_middle u

let eqb (#a: Type) (x: a) (y: a) =
  u2b (x == y)
/
prims.fst.checked FStar.Pervasives.fsti.checked FStar.IndefiniteDescription.fsti.checked
Spec.Ubool.fst
x: a -> y: a -> Prims.GTot Prims.bool
Prims.op_Negation Spec.Ubool.eqb Prims.bool
let neqb (#a: Type) (x y: a) =
  
not (eqb x y)