~/jendhub

def succ_zero

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:34

import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as Nat
import Base

34def succ_zero(+n: Nat, e: {1n+n == 0n : Nat}) -> Empty:
35  zero_succ(n, Equal.sym(Nat, 1n+n, 0n, e))

Uses (4)

Used by (15)