add example showing why we cannot simply extract the witness from TerminatesWith...