From b21e69503571272a5f35cf84c731994f3e921a3a Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 29 Nov 2022 14:36:13 +0000
Subject: Move indexed setoids and functions out of Soat.

---
 src/Soat/FirstOrder/Term.idr | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'src/Soat/FirstOrder/Term.idr')

diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 2712c88..07ab248 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -1,14 +1,13 @@
 module Soat.FirstOrder.Term
 
-import Control.Relation
+import Data.Morphism.Indexed
+import Data.Setoid.Indexed
 
 import Soat.Data.Product
 import Soat.FirstOrder.Algebra
 import Soat.FirstOrder.Signature
-import Soat.Relation
 
 %default total
-%hide Control.Relation.Equivalence
 
 public export
 data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
-- 
cgit v1.2.3