Allow substitutions of locals using the same memory as that used by a Pr

[oskgo]

Before, the following would fail:

require import Real.

module M = {var x: bool proc p()={}}.

lemma L (&m: {b:bool}): b{m}= true => Pr[M.p()@&m:true] = 1%r. 
proof. move => ->>.

We still prevent it in the case where the substitution uses a global, because in that case we'd be erasing information:

lemma L (&m: {b:bool}): M.x{m}= true => Pr[M.p()@&m:true] = 1%r. 
proof. move => ->>. (* This fails to substitute *)

This makes progress and /> more aggressive, which makes it a breaking change. It also fixes some bugs when nesting Pr formulas inside other program logic formulas:

lemma L: phoare[M.p{&m}: true ==> Pr[M.p()@&m:true] = 1%r] = 1%r.
proof.
proc. (* This line used to cause a memory clash anomaly *)

[strub]

Do not use catch all.