xsimpl is sometimes unsafe

Consider the goal

```
W8ARRAY av a ==>> W8ARRAY av a * &(?loc. av = Loc loc)
```

This goal is easily provable, but applying `xsimpl` reduces it to the unprovable goal `∃loc. av = Loc loc`.

The reason this happens is that `hpullr` applies the rule `hsimpl_prop`, which is

```
∀H' H P. P ∧ H' ==>> H ⇒ H' ==>> H * &P
```

This rule does not seem to account for the possibility that the truth of `P` depends on information in `H`. One way to prevent situations such as the above from happening is to strengthen `hsimpl_prop` to say

```
∀H' H P. (∀h. H h ⇒ P) ∧ H' ==>> H ⇒ H' ==>> H * &P
```

However, this would come at the cost of slightly noisier subgoals for the 99% of situations where `H` is not needed to prove `P`.

The purpose of this issue is to discuss whether making this change would be desirable. My own feeling is yes, mostly because I would expect a tactic with "simp" in its name to be safe.