module Unsolved-meta-in-postulate where

postulate P : _