Substitution in statement is incorrect.

[bgregoir]

require import AllCore.

module S = {
  proc f(x:int) = { }

  proc g (x:int) = { return x;}
 
}.

lemma eager_f_sample y : eager [
  S.f(y);, S.g ~ S.g, S.f(y); :
    ={x} ==> ={res} ].
proof.
eager proc; inline *; swap{1} 1; sim.
qed.

lemma eager_f_sample' z : eager [
  S.f(z);, S.g ~ S.g, S.f(z); :
    ={x} ==> ={res} ].
proof.
apply (eager_f_sample z).
qed.

The problem come from the substitution, the forall use F_subst.bind_local to substitute "y" by "z", but it should also
bind using F_subst.bind_elocal.

[bgregoir]

Remark that:

   have := eager_f_sample z. 

Raise "anomaly: EcLib.EcCoreGoal.InvalidGoalShape"

[bgregoir]

Another problem commit from ecSubst this time (I think).
require import AllCore.

section SC.
module S = {
  proc f(x:int) = { }

  proc g (x:int) = { return x;}
 
}.

lemma eager_f_sample y : eager [
  S.f(y);, S.g ~ S.g, S.f(y); :
    ={x} ==> ={res} ].
proof.
eager proc; inline *; swap{1} 1; sim.
qed.

end section SC.

op b : bool.

lemma toto : b.
have := eager_f_sample.
move=> /= h.
have := h 1.