diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
index dab052df..2d8108b1 100644
--- a/lib/Haskell/Prelude.agda
+++ b/lib/Haskell/Prelude.agda
@@ -125,7 +125,7 @@ lookup x []              = Nothing
 lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
 
 
-subst0 : (p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
+subst0 : (@0 p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
 subst0 p refl z = z
 {-# COMPILE AGDA2HS subst0 transparent #-}