law slot_small_t

lawful-arrays@0.1.0.0 · proof_index.bend:421

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

421law slot_small_t:
422  for +i: U32
423  for +d: Nat
424  for +h: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool}
425  {D.slot(i, d) == U32.to_nat(i) : Nat}