(P x)
     : Prop
(R x x)
     : Prop
[x:foo; n:nat](x n)
     : foo ->nat ->nat