gdp-0.0.3.0: Reason about invariants and preconditions with ghosts of departed proofs.