diff --git a/src/Analysis/Measure/OuterMeasureRing.ard b/src/Analysis/Measure/OuterMeasureRing.ard
index 740ce18b..a673f767 100644
--- a/src/Analysis/Measure/OuterMeasureRing.ard
+++ b/src/Analysis/Measure/OuterMeasureRing.ard
@@ -43,6 +43,7 @@
   | norm_negative => pmap norm neative=id
   | norm_+ => rewrite +_diff $ norm-outer-measure LowerRealAbMonoid.<=∘ LowerRealAbMonoid.<=_+ (norm-outer-mono diff_<=) (norm-outer-mono diff_<=)
 
+-- TODO: Replace with relative completion
 \class ExtendedMeasure \noclassifying (R : LowerPseudoNormedAbGroup) (M : PseudoPremeasureRing) (inc : AddGroupHom M R) (comp : \Pi (a : M) -> norm a LowerRealAbMonoid.<= norm (inc a)) {
   \func IsMeasurable (a : R) : \Prop
     => ∃ (F : ProperFilter M) (R.IsFilterLimit (SetFilter-map inc F) a)
@@ -93,6 +94,7 @@
       | isCauchyFilter {C} => measurable-cauchy (filter-limit-cauchy al) {C}
     } \in (CompleteCoverSpace.filter-point CF, inP (F, al, CompleteCoverSpace.filter-point-limit))
 
+  {-
   \lemma measurable-closed {a b c : R} (op : M -> M -> M) (am : IsMeasurable a) (bm : IsMeasurable b) : IsMeasurable c \elim am, bm
     | inP (F,Fa), inP (G,Gb) =>
       \let H : ProperFilter M => \new ProperFilter {
@@ -118,5 +120,5 @@
         }
       }
       \in inP (H, \lam {W} Wo Wc => inP {?})
-
+  -}
 }