diff --git a/lib/Haskell/Law/Equality.agda b/lib/Haskell/Law/Equality.agda
index 1ace524e..2d307bdc 100644
--- a/lib/Haskell/Law/Equality.agda
+++ b/lib/Haskell/Law/Equality.agda
@@ -57,3 +57,11 @@ _∎ _ = refl
 
 syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
 syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z
+
+
+-------------------------------------------------
+-- Utility Functions
+
+subst0 : {@0 a : Set} (@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 #-}
diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
index dbedf71c..78cca2bc 100644
--- a/lib/Haskell/Prelude.agda
+++ b/lib/Haskell/Prelude.agda
@@ -100,7 +100,6 @@ error {i = ()} err
 errorWithoutStackTrace : {@0 @(tactic absurd) i : ⊥} → String → a
 errorWithoutStackTrace {i = ()} err
 
-
 -------------------------------------------------
 -- More List functions
 --   These uses Eq, Ord, or Foldable, so can't go in Prim.List without
@@ -124,6 +123,7 @@ lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
 lookup x []              = Nothing
 lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
 
+
 -------------------------------------------------
 -- Unsafe functions