def AP.nat_t

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base

34def AP.nat_t(n: Nat) -> Type:
35  match n:
36    case 0n:
37      Unit
38    case 1n+p:
39      Empty

Uses (3)