diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 9671bb6..5702eee 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -52,19 +52,19 @@ export
 tests : Test
 tests = "equality & subtyping" :- [
     "universes" :- [
-        testEq "★₀ ≡ ★₀" $
-          equalT (TYPE 0) (TYPE 0),
-        testNeq "★₀ ≢ ★₁" $
-          equalT (TYPE 0) (TYPE 1),
-        testNeq "★₁ ≢ ★₀" $
-          equalT (TYPE 1) (TYPE 0),
-        testEq "★₀ <: ★₀" $
-          subT (TYPE 0) (TYPE 0),
-        testEq "★₀ <: ★₁" $
-          subT (TYPE 0) (TYPE 1),
-        testNeq "★₁ ≮: ★₀" $
-          subT (TYPE 1) (TYPE 0)
-      ],
+      testEq "★₀ ≡ ★₀" $
+        equalT (TYPE 0) (TYPE 0),
+      testNeq "★₀ ≢ ★₁" $
+        equalT (TYPE 0) (TYPE 1),
+      testNeq "★₁ ≢ ★₀" $
+        equalT (TYPE 1) (TYPE 0),
+      testEq "★₀ <: ★₀" $
+        subT (TYPE 0) (TYPE 0),
+      testEq "★₀ <: ★₁" $
+        subT (TYPE 0) (TYPE 1),
+      testNeq "★₁ ≮: ★₀" $
+        subT (TYPE 1) (TYPE 0)
+    ],
 
     "pi" :- [
       -- ⊸ for →₁, ⇾ for →₀
@@ -129,39 +129,44 @@ tests = "equality & subtyping" :- [
     todo "term d-closure",
 
     "free var" :- [
-        testEq "A ≡ A" $
-          equalE (F "A") (F "A"),
-        testNeq "A ≢ B" $
-          equalE (F "A") (F "B"),
-        testEq "A <: A" $
-          subE (F "A") (F "A"),
-        testNeq "A ≮: B" $
-          subE (F "A") (F "B")
-      ],
+      testEq "A ≡ A" $
+        equalE (F "A") (F "A"),
+      testNeq "A ≢ B" $
+        equalE (F "A") (F "B"),
+      testEq "A <: A" $
+        subE (F "A") (F "A"),
+      testNeq "A ≮: B" $
+        subE (F "A") (F "B")
+    ],
 
-    todo "bound var",
+    "bound var" :- [
+      testEq "#0 ≡ #0" $
+        equalE (BV 0) (BV 0) {n = 1},
+      testNeq "#0 ≢ #1" $
+        equalE (BV 0) (BV 1) {n = 2}
+    ],
 
     "application" :- [
-        testEq "f [a] ≡ f [a]" $
-          equalE (F "f" :@ FT "a") (F "f" :@ FT "a"),
-        testEq "f [a] <: f [a]" $
-          subE (F "f" :@ FT "a") (F "f" :@ FT "a"),
-        testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A)  (β)" $
-          equalE
-            ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
-              :@ FT "a")
-            (E (FT "a" :# FT "A") :# FT "A"),
-        testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ a  (βυ)" $
-          equalE
-            ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
-              :@ FT "a")
-            (F "a"),
-        testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
-          subE
-            ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
-              :@ FT "a")
-            (F "a")
-      ],
+      testEq "f [a] ≡ f [a]" $
+        equalE (F "f" :@ FT "a") (F "f" :@ FT "a"),
+      testEq "f [a] <: f [a]" $
+        subE (F "f" :@ FT "a") (F "f" :@ FT "a"),
+      testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A)  (β)" $
+        equalE
+          ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
+            :@ FT "a")
+          (E (FT "a" :# FT "A") :# FT "A"),
+      testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ a  (βυ)" $
+        equalE
+          ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
+            :@ FT "a")
+          (F "a"),
+      testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
+        subE
+          ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
+            :@ FT "a")
+          (F "a")
+    ],
 
     todo "annotation",