law cnt_range

minebender-game@1.0.0.0 · proof_gen.bend:694

import Base

694# Each number below n appears in range(n) once.
695law cnt_range:
696  for +i: Nat
697  for +n: Nat
698  {cnt(i, List.range(n)) == Bool.pick(Nat, Nat.is_lt(i, n), 1n, 0n) : Nat}