diff --git a/examples/misc.quox b/examples/misc.quox
index 8188a1d..bbad8e6 100644
--- a/examples/misc.quox
+++ b/examples/misc.quox
@@ -9,11 +9,18 @@ def void : 0.(A : ★) → 0.False → A =
 def0 All : (A : ★) → (0.A → ★) → ★¹ =
   λ A P ⇒ (x : A) → P x
 
-def cong :
-    0.(A : ★) → 0.(P : 0.A → ★) → (p : All A P) →
-    0.(x y : A) → (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
+def0 cong :
+    (A : ★) → (P : 0.A → ★) → (p : All A P) →
+    (x y : A) → (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
   λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖)
 
+def0 coherence :
+    (A B : ★) → (AB : A ≡ B : ★) → (x : A) →
+    Eq (𝑖 ⇒ AB @𝑖) x (coe (𝑖 ⇒ AB @𝑖) x) =
+  λ A B AB x ⇒
+    δ 𝑗 ⇒ coe (𝑖 ⇒ AB @𝑖) @0 @𝑗 x
+
+
 def0 eq-f :
     0.(A : ★) → 0.(P : 0.A → ★) →
     0.(p : All A P) → 0.(q : All A P) →
@@ -35,29 +42,29 @@ def trans : 0.(A : ★) → 0.(x y z : A) →
 
 def appω : 0.(A B : ★) → ω.(f : A → B) → [ω.A] → [ω.B] =
   λ A B f x ⇒
-  case x return [ω.B] of { [x'] ⇒ [f x'] };
+  case x return [ω.B] of { [x'] ⇒ [f x'] }
 
 
 def0 Sing : (A : ★) → A → ★ =
-  λ A x ⇒ (val : A) × [0. val ≡ x : A];
+  λ A x ⇒ (val : A) × [0. val ≡ x : A]
 
 namespace sing {
 
 def val : 0.(A : ★) → 0.(x : A) → Sing A x → A =
   λ A _ sg ⇒
-  case sg return A of { (x, eq) ⇒ case eq return A of { [_] ⇒ x } };
+  case sg return A of { (x, eq) ⇒ case eq return A of { [_] ⇒ x } }
 
 def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A =
   λ A x sg ⇒
   case sg return sg' ⇒ val A x sg' ≡ x : A of { (x', eq) ⇒
     case eq return eq' ⇒ val A x (x', eq') ≡ x : A of { [eq'] ⇒ eq' }
-  };
+  }
 
 def app : 0.(A B : ★) → 0.(x : A) →
           (f : A → B) → Sing A x → Sing B (f x) =
   λ A B x f sg ⇒
   case sg return Sing B (f x) of { (x_, eq) ⇒
     case eq return Sing B (f x) of { [eq] ⇒ (f x_, [δ 𝑖 ⇒ f (eq @𝑖)]) }
-  };
+  }
 
 }