From bf07a9fe3ee4ff06fe186e33221f7f91871b9217 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 6 Jun 2023 12:25:26 +0100
Subject: Write an encoding for data types.

---
 src/Total/Term.idr | 9 +++++++++
 1 file changed, 9 insertions(+)

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

diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index 1530981..d4da92a 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -321,6 +321,15 @@ baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin)
 
 -- Substitution
 
+export
+substId : (t : Term ctx ty) -> subst t (Base Id) = t
+substId (Var i) = Refl
+substId (Abs t) = cong Abs $ trans (sym $ substCong t Base) (substId t)
+substId (App t u) = cong2 App (substId t) (substId u)
+substId Zero = Refl
+substId (Suc t) = cong Suc (substId t)
+substId (Rec t u v) = cong3 Rec (substId t) (substId u) (substId v)
+
 export
 substHomo :
   (t : Term ctx ty) ->
-- 
cgit v1.2.3