erase p in the subst0

and move to a different part of the file

lib/Haskell/Prelude.agda

@@ -101,6 +101,10 @@ errorWithoutStackTrace : {@0 @(tactic absurd) i : ⊥} → String → a
 errorWithoutStackTrace {i = ()} err
 
 
+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 #-}
+
 -------------------------------------------------
 -- More List functions
 --   These uses Eq, Ord, or Foldable, so can't go in Prim.List without
@@ -125,10 +129,6 @@ 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 p refl z = z
-{-# COMPILE AGDA2HS subst0 transparent #-}
-
 -------------------------------------------------
 -- Unsafe functions