From a618facb653fa08e41215bb6ede2849de20c8c4d Mon Sep 17 00:00:00 2001
From: Bohdan <b.liesnikov+git@gmail.com>
Date: Mon, 22 Jan 2024 11:51:25 +0100
Subject: [PATCH] move subst0 to Law.Equality

---
 lib/Haskell/Law/Equality.agda | 8 ++++++++
 lib/Haskell/Prelude.agda      | 5 -----
 2 files changed, 8 insertions(+), 5 deletions(-)

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 90919e6c..78cca2bc 100644
--- a/lib/Haskell/Prelude.agda
+++ b/lib/Haskell/Prelude.agda
@@ -100,11 +100,6 @@ error {i = ()} err
 errorWithoutStackTrace : {@0 @(tactic absurd) i : ⊥} → String → a
 errorWithoutStackTrace {i = ()} err
 
-
-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 #-}
-
 -------------------------------------------------
 -- More List functions
 --   These uses Eq, Ord, or Foldable, so can't go in Prim.List without