(P x)
     : Prop
(R x x)
     : Prop