wp_cas_suc fails with total weakest precondition
As the title mentions wp_cas_suc fails with total weakest precondition. The reason seems to be that the well-formedness assumption on what is stored at the location is not discharged correctly since I can make it go through with
wp_apply (twp_cas_suc with "Hpt"); [by left | ].
instead of wp_cas_suc.
See the attached file for a complete example.