pr : Π {A}, A → A → A
pr a b : N
pr a b : N