{-# LANGUAGE RankNTypes #-}

-- [Definitions]
-- Not
newtype Not p = Not (forall q. p -> q)

-- …