Restrictions of module aliases are not checked correctly #1234

module type T = {
  proc p(): bool
}.

module True = {proc p()={return true;}}.

module False = {proc p()={return false;}}.

module type F (M: T) = {
  proc p(): bool {} (* restricted to not make any calls *)
}.

lemma L1 (F<:F): equiv[F(True).p ~F(False).p : ={glob F} ==> ={res}].
proof. proc*; call (: true); auto => />. qed.

module (C: F) (M: T) = M.

require import Real.

lemma bad: false.
suff//: forall &m, 1%r = 2%r.
move => &m.
have->:1%r=Pr[C(True).p() @&m: true].
- by byphoare => //; proc.
rewrite Pr[mu_split res] /=.
have->:Pr[C(True).p()@&m:!res]=Pr[C(False).p()@&m:!res].
- byequiv (L1 C) => //.
have->:Pr[C(True).p()@&m:res]=1%r by byphoare => //; proc.
have->:Pr[C(False).p()@&m:!res]=1%r by byphoare => //; proc.
done.
qed.