diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 6a058c7..639fc36 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -196,16 +196,16 @@ zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
 
 
 export
-lengthPrf : Telescope _ from to -> (len : Nat ** len + from = to)
-lengthPrf [<]        = (0 ** Refl)
+lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
+lengthPrf [<]        = Element 0 Refl
 lengthPrf (tel :< _) =
-  let len = lengthPrf tel in (S len.fst ** cong S len.snd)
+  let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
 
 export
-lengthPrf0 : Context _ to -> (len : Nat ** len = to)
+lengthPrf0 : Context _ to -> Subset Nat (\len => len = to)
 lengthPrf0 ctx =
-  let (len ** prf) = lengthPrf ctx in
-  (len ** rewrite sym $ plusZeroRightNeutral len in prf)
+  let len = lengthPrf ctx in
+  Element len.fst (rewrite sym $ plusZeroRightNeutral len.fst in len.snd)
 
 public export %inline
 length : Telescope {} -> Nat