def Nat.disc_z

lawful-words@0.1.0.0 · proof_nat.bend:102

import Base

102def Nat.disc_z(n: Nat) -> Type:
103  match n:
104    case 0n:
105      Empty
106    case 1n+p:
107      Unit