~/jendhub

def wsh.z0

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:380

import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
import Base

380def wsh.z0(x: Nat, e: {Nat.is_eq(x, 0n) == True{} : Bool}) -> {x == 0n : Nat}:
381  match x:
382    case 0n:
383      {==}
384    case 1n+ +p:
385      Empty.absurd({1n+p == 0n : Nat}, wn.ft(e))

Uses (5)

Used by (1)