2 files changed, 44 insertions, 0 deletions
diff --git a/src/Core/Term/Substitution.idr b/src/Core/Term/Substitution.idr
index 6846d80..abeb487 100644
--- a/src/Core/Term/Substitution.idr
+++ b/src/Core/Term/Substitution.idr
@@ -30,6 +30,16 @@ index (Wkn thin) i = Var i `Over` thin
 index (sub :< t) FZ = t
 index (sub :< t) (FS i) = index sub i
 
+export
+indexCong :
+  {0 sub1, sub2 : Subst m n} ->
+  sub1 =~= sub2 ->
+  (i : Fin m) ->
+  index sub1 i =~= index sub2 i
+indexCong Refl i = Refl
+indexCong (prf :< prf') FZ = prf'
+indexCong (prf :< prf') (FS i) = indexCong prf i
+
 -- Weakening -------------------------------------------------------------------
 
 public export
@@ -37,6 +47,15 @@ wkn : Subst k m -> m `Thins` n -> Subst k n
 wkn (Wkn thin') thin = Wkn (thin . thin')
 wkn (sub :< t) thin = wkn sub thin :< wkn t thin
 
+export
+wknCong :
+  {0 sub1, sub2 : Subst k m} ->
+  sub1 =~= sub2 ->
+  (thin : m `Thins` n) ->
+  wkn sub1 thin =~= wkn sub2 thin
+wknCong Refl thin = Refl
+wknCong (prf :< prf') thin = wknCong prf thin :< wknCong prf' thin
+
 -- Constructors ----------------------------------------------------------------
 
 public export
@@ -52,3 +71,18 @@ subst Set sub = Set
 subst (Pi t u) sub = Pi (subst t sub) (subst u $ lift sub)
 subst (Abs t) sub = Abs (subst t $ lift sub)
 subst (App t u) sub = App (subst t sub) (subst u sub)
+
+export
+substCong :
+  (t : Term m) ->
+  {0 sub1, sub2 : Subst m n} ->
+  sub1 =~= sub2 ->
+  subst t sub1 = subst t sub2
+substCong (Var i) prf = indexCong prf i
+substCong Set prf = Refl
+substCong (Pi t u) prf =
+  cong2 Pi
+    (substCong t prf)
+    (substCong u $ wknCong prf (drop $ id n) :< Refl)
+substCong (Abs t) prf = cong Abs (substCong t $ wknCong prf (drop $ id n) :< Refl)
+substCong (App t u) prf = cong2 App (substCong t prf) (substCong u prf)
diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr
index 0bc6dcf..824439a 100644
--- a/src/Core/Term/Thinned.idr
+++ b/src/Core/Term/Thinned.idr
@@ -3,6 +3,8 @@ module Core.Term.Thinned
 import Core.Term
 import Core.Thinning
 
+import Syntax.PreorderReasoning
+
 %prefix_record_projections off
 
 infix 4 =~=
@@ -32,3 +34,11 @@ t =~= u = expand t = expand u
 public export
 wkn : Thinned m -> m `Thins` n -> Thinned n
 wkn t thin = { thin $= (thin .) } t
+
+export
+wknCong : t =~= u -> (thin : m `Thins` n) -> wkn t thin =~= wkn u thin
+wknCong {t = t `Over` thin1, u = u `Over` thin2} prf thin = Calc $
+  |~ wkn t (thin . thin1)
+  ~~ wkn (wkn t thin1) thin ...(sym $ wknHomo t thin1 thin)
+  ~~ wkn (wkn u thin2) thin ...(cong (flip wkn thin) prf)
+  ~~ wkn u (thin . thin2)   ...(wknHomo u thin2 thin)