Add progress bit to WP.

I indexed WP by a progress bit, making safety optional so that one can link against code that might get stuck. The meaning of WP e @ E {{ Φ }} has not changed. The judgment WP e @ E ?{{ Φ }} permits e to get stuck. The judgment WP e @ p; E {{ Φ }} where p : bool is useful when either works. Similar notations exist for Texan and Hoare triples. There are lemmas for forgetting progress bits (e.g., converting a safe triple to a triple that might get stuck) and for lifting stuck expressions.

The heap_lang tactics continue to assume safe WP.

I had to revert the recent weakening of atomic e so that wp_atomic goes through.