val for_all_range (n: nat) (f: (i: nat{i < n} -> GTot bool)) : GTot bool
val for_all_range (n: nat) (f: (i: nat{i < n} -> GTot bool)) : GTot bool
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)
module Util.Range

open Spec.Ubool
/
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 Prims.bool) -> Prims.GTot Prims.bool
Prims.nat Prims.b2t Prims.op_LessThan Prims.bool Prims.op_Equality Prims.int Prims.op_AmpAmp Prims.op_Subtraction Util.Range.for_all_range
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)