\bmeta Points to keep in mind:
\bit


\item Does exhaustivity hold for any closed simple term? (No) Provide
  a counterexample. Tightening fails for non-simple closed terms, \ie
  for intuitionistic application.



\enit
\emeta