From 52b9e2f139444f012f3610e60321e4336d888bec Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 23 Apr 2023 14:33:18 +0100
Subject: Prove escape theorems.

---
 src/Core/Generic.idr | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/Core/Generic.idr')

diff --git a/src/Core/Generic.idr b/src/Core/Generic.idr
index c2bd1f4..4563063 100644
--- a/src/Core/Generic.idr
+++ b/src/Core/Generic.idr
@@ -118,6 +118,10 @@ interface IsEq (0 eq : Equality) where
     ---
     eq.TypeEq {n} env (Pi a b) (Pi c d)
 
+export
+ntrlEqImpliesTypeEq : IsEq eq => eq.NtrlEq {n = k} env n m Set -> eq.TypeEq env n.fst m.fst
+ntrlEqImpliesTypeEq = termEqImpliesTypeEq . ntrlEqImpliesTermEq
+
 -- Instance 1 ------------------------------------------------------------------
 
 public export
-- 
cgit v1.2.3