Improving the default pre-condition on `hoare` subgoals from `conseq` in pRHL

[fdupress]

When doing conseq (: P ==> Q) (: _ ==> Q1). in pRHL (with Q1 a Hoare postcondition), we currently use true as the precondition for the Hoare subgoal about the left-hand side program. When facts from P are useful in proving Q1, those need to be repeated—which is unfortunate.

A more general thing would be to generate the subgoal (: P' ==> Q) where P' is P, existentially quantifying on the value of the variables in the right memory.

(This should also be done for the RHS variant and for the variant that refines to Hoare goals on both sides.)