Mention Ghosts of Departed Proofs

[Chris Warburton]

GODP is a way of using phantom types to encode proofs, useful as
preconditions for functions. The paper begins with a simple example of
non-empty lists, eventually working up to a standalone library of
natural-deduction proofs, and GHC type-checker plugins which implement
proof tactics.

This is a clear use-case for theory exploration results.