diff --git a/examples/misc.quox b/examples/misc.quox
index 5ae7e76..f6ba7d9 100644
--- a/examples/misc.quox
+++ b/examples/misc.quox
@@ -33,4 +33,4 @@ def sym : 0.(A : ★₀) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A =
 def trans : 0.(A : ★₀) → 0.(x y z : A) →
             ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
   λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒
-    comp [A] @0 @1 (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @0 };
+    comp [A] @0 @1 (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 };