val for_all_range_ubool (n: nat) (f: (i: nat{i < n} -> GTot ubool)) : GTot ubool
val for_all_range_ubool (n: nat) (f: (i: nat{i < n} -> GTot ubool)) : GTot ubool
let rec for_all_range_ubool (n: nat) (f: (i: nat{i < n}) -> GTot ubool) : GTot ubool =
  if n = 0 then True else (f (n - 1) /\ for_all_range_ubool (n - 1) f)
module Util.Range

open Spec.Ubool

let rec for_all_range (n: nat) (f: (i: nat{i < n}) -> GTot bool) : GTot bool =
  if n = 0 then true else (f (n - 1) && for_all_range (n - 1) f)
/
Spec.Ubool.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
Util.Range.fsti
n: Prims.nat -> f: (i: Prims.nat{i < n} -> Prims.GTot Spec.Ubool.ubool)
  -> Prims.GTot Spec.Ubool.ubool
Prims.nat Prims.b2t Prims.op_LessThan Spec.Ubool.ubool Prims.op_Equality Prims.int Prims.l_True Prims.bool Prims.l_and Prims.op_Subtraction Util.Range.for_all_range_ubool
let rec for_all_range_ubool (n: nat) (f: (i: nat{i < n} -> GTot ubool)) : GTot ubool =
  
if n = 0 then True else (f (n - 1) /\ for_all_range_ubool (n - 1) f)