diff --git a/FEM/FE_LagP.v b/FEM/FE_LagP.v
index 830731f566fb070fe16ed743c68093c334b66900..e432f3a489ea8bb52aee214de9cd6da456d5bfba 100644
--- a/FEM/FE_LagP.v
+++ b/FEM/FE_LagP.v
@@ -702,11 +702,12 @@ f_equal.
 apply T_geom_transports_nodes; easy.
 (* *)
 rewrite shape_fun_L_cur_eq.
-(* FIXME HM 19/02/24: pourquoi on ne peut pas utiliser 
-  shape_fun_cur_correct_rev ? *)
-erewrite shape_fun_cur_correct_rev2; easy.
+rewrite (shape_fun_cur_correct_rev FE_LagPk_d_ref _ vtx_cur); easy.
 Qed.
 
+
+
+
 End FE_Lagrange_ref_Pk_d_fact.
 
 (* Note du 4/7/23
diff --git a/FEM/FE_simplex.v b/FEM/FE_simplex.v
index 03a95036a383da6043d19e3983b8cd4ca2a3806a..6bd0965d501d564221b330759dcbcf476927b8bf 100644
--- a/FEM/FE_simplex.v
+++ b/FEM/FE_simplex.v
@@ -408,18 +408,12 @@ apply H2.
 Qed.
 
 Lemma shape_fun_cur_correct_rev : forall i : 'I_(ndof FE_cur), 
-  shape_fun_ref i = cur_to_ref (shape_fun_cur i).
+  shape_fun FE_ref i = cur_to_ref (shape_fun_cur i).
 Proof.
 intros i; rewrite shape_fun_cur_correct.
 apply cur_to_ref_comp. 
 Qed.
 
-Lemma shape_fun_cur_correct_rev2 :
-  shape_fun_ref = (fun i x_ref => shape_fun_cur i (T_geom vtx_cur x_ref)).
-Proof.
-apply extF; intros i.
-apply shape_fun_cur_correct_rev.
-Qed.
 
 Definition local_interp_cur : FRd d_cur -> FRd d_cur := 
   fun v => local_interp FE_cur v.