diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml
index 14368120d..cb99d5b5f 100644
--- a/src/ecCoreSubst.ml
+++ b/src/ecCoreSubst.ml
@@ -95,6 +95,10 @@ let bind_elocals (s : f_subst) (esloc : expr Mid.t) : f_subst =
 
 (* -------------------------------------------------------------------- *)
 let f_bind_local (s : f_subst) (x : ident) (t : form) : f_subst =
+  let s =
+    match EcCoreFol.expr_of_form t with
+    | e -> bind_elocal s x e
+    | exception EcCoreFol.CannotTranslate -> s in
   let fs_loc = Mid.add x t s.fs_loc in
   let fs_fv = fv_union (f_fv t) s.fs_fv in
   { s with fs_loc; fs_fv; }
diff --git a/src/ecSubst.ml b/src/ecSubst.ml
index 2faa40679..023b751c2 100644
--- a/src/ecSubst.ml
+++ b/src/ecSubst.ml
@@ -217,6 +217,10 @@ let fresh_elocals_opt (s : subst) (locals : (EcIdent.t option * ty) list) =
   List.fold_left_map fresh_elocal_opt s locals
 
 let add_flocal (s : subst) (x : EcIdent.t) (f : EcCoreFol.form) =
+  let s =
+    match EcCoreFol.expr_of_form f with
+    | e -> add_elocal s x e
+    | exception EcCoreFol.CannotTranslate -> s in
   { s with sb_flocal = Mid.add x f s.sb_flocal }
 
 let add_flocals (s : subst) (xs : EcIdent.t list) (fs : EcCoreFol.form list) =
@@ -1215,4 +1219,3 @@ let inv_rebind (inv : inv) (ms : memory list) : inv =
   | Inv_ts ts, [ml; mr] -> Inv_ts (ts_inv_rebind ts ml mr)
   | Inv_hs hs, [m] -> Inv_hs (hs_inv_rebind hs m)
   | _, _ -> assert false
-
diff --git a/tests/eager_call_instanciate.ec b/tests/eager_call_instanciate.ec
new file mode 100644
index 000000000..23756a68d
--- /dev/null
+++ b/tests/eager_call_instanciate.ec
@@ -0,0 +1,33 @@
+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.
+
+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.
+
+end section SC.
+
+op b : bool.
+
+lemma toto : b.
+have /= h := eager_f_sample.
+have := h 1.
+admitted.
+