def un.pred
import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOFimport Base
44def un.pred(n: Nat) -> Nat:
45 match n:
46 case 0n:
47 0n
48 case 1n+p:
49 p
import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOFimport Base
44def un.pred(n: Nat) -> Nat:
45 match n:
46 case 0n:
47 0n
48 case 1n+p:
49 p