-- Prop has been removed from the language
module PropNoMore where

postulate
  X : Prop