diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean
index f36cb58..c87fa76 100644
--- a/Nevanlinna/laplace2.lean
+++ b/Nevanlinna/laplace2.lean
@@ -61,10 +61,12 @@ theorem LaplaceIndep
   have g : (i : Fin 2) → ι → E := by exact fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j))
   have A : (i : Fin 2) → Finset ι := by exact fun _ ↦ Finset.univ
 
-  let X := ContinuousMultilinearMap.map_sum_finset 
+  let X := ContinuousMultilinearMap.map_sum
     (iteratedFDeriv ℝ 2 f z)
     (fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j)))
-    (fun _ ↦ Finset.univ)
+
+  --
+  --  (fun _ ↦ Finset.univ)
   simp at X
   
   sorry