From 60df32ffd5b88498e4634649509bbd0810421004 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 11 Jul 2023 16:25:24 +0100
Subject: Begin big unification proof.

---
 src/Data/Term.idr | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/Data/Term.idr')

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 4b0ac3e..ebb7b00 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -30,6 +30,9 @@ export
 varIsVar : (x : SFin (S n)) -> Var' x = Var x
 varIsVar x = Refl
 
+export
+Uninhabited (Op op ts = Var x) where uninhabited prf impossible
+
 -- Substitution ----------------------------------------------------------------
 
 export
-- 
cgit v1.2.3