diff --git a/test/probability/rand_with_trace.lean b/test/probability/rand_with_trace.lean
index 1b0c09f9..e7c28c61 100644
--- a/test/probability/rand_with_trace.lean
+++ b/test/probability/rand_with_trace.lean
@@ -1,4 +1,5 @@
 import SciLean.Probability.RandWithTrace
+import SciLean.Analysis.Scalar.FloatAsReal
 
 open SciLean Rand MeasureTheory
 
@@ -39,10 +40,6 @@ info: tt :
 #check tt
 
 
-instance (n:Nat) [MeasureSpace X] : MeasureSpace {a : Array X // a.size = n} := sorry
-instance (n:Nat) [MeasureSpace X] : MeasureSpace (ArrayN X n) := sorry
-
-
 /--
 info: fun x =>
   pdf Float