module Data.PNat where
data PNat = Z | S PNat