Define properties of substitutions.

1 files changed, 11 insertions, 0 deletions

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
@@ -80,6 +87,10 @@ 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)} ->
   {0 us : Vect j (Term sig n)} ->