diff --git a/src/Typed.lagda b/src/Typed.lagda
index 4af31021..2058edea 100644
--- a/src/Typed.lagda
+++ b/src/Typed.lagda
@@ -676,6 +676,7 @@ the proof works. Bugger!
     M⊆ = trans-⊆ ⊆-++₁ (trans-⊆ (⊆-++₂ {free L}) ⊆xs)
     N⊆ = trans-⊆ ⊆-++₂ (trans-⊆ (⊆-++₂ {free L}) ⊆xs)
 ⊢rename ⊢σ ⊆xs (⊢Y ⊢M)     =  ⊢Y (⊢rename ⊢σ ⊆xs ⊢M)
+-}
 \end{code}