def zero_succ

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

30def zero_succ(+n: Nat, e: {0n == 1n+n : Nat}) -> Empty:
31  %e : L.truth(is_zero(_))
32  Unit{}