definition pnat : Type₁ :=
{n | n > 0}
inductive prod : Type → Type → Type
constructors:
prod.mk : Π {A} {B}, A → B → A × B