From 6b637a6d2954e77985e24bbd17f3697eb6f8238a Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 7 Jul 2023 17:36:37 +0100
Subject: Define properties of substitutions.

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

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

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 2afc774..3b16f38 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -38,6 +38,13 @@ public export
 0 (.=.) : Rel (Fin k -> Term sig n)
 f .=. g = (i : Fin k) -> f i = g i
 
+export
+subCong : {f, g : Fin k -> Term sig n} -> f .=. g -> (t : Term sig k) -> f <$> t = g <$> t
+subCong prf (Var i) = prf i
+subCong prf (Op op ts) =
+  cong (Op op) $
+  mapExtensional (f <$>) (g <$>) (\t => subCong prf (assert_smaller ts t)) ts
+
 -- Substitution is Monadic -----------------------------------------------------
 
 export
@@ -79,6 +86,10 @@ export
 opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
 opInjectiveLen Refl = Refl
 
+export
+opInjectiveTs' : {0 ts, us : Vect k (Term sig n)} -> (prf : Op op ts = Op op us) -> ts = us
+opInjectiveTs' Refl = Refl
+
 export
 opInjectiveTs :
   {0 ts : Vect k (Term sig n)} ->
-- 
cgit v1.2.3