Stronger precondition in pRHL tactics eager-seq and eager-while

[loutr]

This PR provides a stronger precondition to one of the premises of the eager seq pRHL tactic. Concretely, premise (c)'s precondition is strengthened from

  (c) c₁' ~ c₁' : Eq ==> R₁

to

  (c) c₁' ~ c₁' : Eq /\ ∃m. P m m₂ ==> R₁

A similar adjustment is derived for the eager while tactic (its soundness proof is based on eager seq).
Some utility functions to manipulate and existentially generalise ss_inv and ts_inv structs are added. These utility functions are not all used in this PR but are added for symmetry with similar universally-generalising utility functions.

The purpose of this strengthening is to allow invariants (notably in the eager while tactic) to carry more information than equalities; which were otherwise limited by the fact that one had to prove c' ~ c' : Eq ==> I.