From f910e142ce7c10f8244ecfa40e41756fb8c8a53f Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 9 Jun 2023 16:00:39 +0100
Subject: Use co-deBruijn syntax in logical relation proof.

Many proofs are still missing. Because they are erased, the program
still runs fine without them.
---
 src/Total/Term.idr | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index 8e3e42a..129662a 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -77,6 +77,7 @@ sub2 . (sub1 :< t) = sub2 . sub1 :< subst t sub2
 
 -- Utilities
 
+export
 cong3 : (0 f : a -> b -> c -> d) -> x1 = x2 -> y1 = y2 -> z1 = z2 -> f x1 y1 z1 = f x2 y2 z2
 cong3 f Refl Refl Refl = Refl
 
-- 
cgit v1.2.3