~/jendhub

def one_when

minebender-game@1.0.0.0 · proof_gen.bend:820

import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
import Base

820def one_when(+i: Nat, +n: Nat, lt: {Nat.is_lt(i, n) == True{} : Bool}) -> {cnt(i, List.range(n)) == 1n : Nat}:
821  Equal.trans(Nat, cnt(i, List.range(n)), Bool.pick(Nat, Nat.is_lt(i, n), 1n, 0n), 1n,
822    cnt_range(i, n),
823    Equal.cong(Bool, Nat, b => Bool.pick(Nat, b, 1n, 0n), Nat.is_lt(i, n), True{}, lt))

Uses (9)

Used by (1)