postulate P : (A : Set) → A → Set X : Set x : X P' : (A : Set) → _ R : Set R = P' _ x P' = P