@hackage gdp0.0.0.1

Reason about invariants and preconditions with ghosts of departed proofs.

gdp: Ghosts of Departed Proofs