1 files changed, 20 insertions, 7 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 5935254..7c2fca1 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -108,21 +108,34 @@ FreeAlgebra : ISetoid sig.T -> Algebra sig
 FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
 
 public export
+bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
+  -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.rel t (env t x) (env' t y))
+  -> {t : sig.T} -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm'
+  -> a.rel t (bindTerm {a = a.raw} env tm) (bindTerm {a = a.raw} env' tm')
+
+public export
+bindTermsCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
+  -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.rel t (env t x) (env' t y))
+  -> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms'
+  -> Pointwise a.rel (bindTerms {a = a.raw} env tms) (bindTerms {a = a.raw} env' tms')
+
+bindTermCong'         cong (Done' i)     = cong _ i
+bindTermCong' {a = a} cong (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong ts)
+
+bindTermsCong' cong []        = []
+bindTermsCong' cong (t :: ts) = bindTermCong' cong t :: bindTermsCong' cong ts
+
+public export
 bindTermCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
   -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm'
   -> a.rel t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
+bindTermCong env = bindTermCong' env.cong
 
 public export
 bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
   -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms'
   -> Pointwise a.rel (bindTerms {a = a.raw} env.func tms) (bindTerms {a = a.raw} env.func tms')
-
-bindTermCong         env (Done' i)     = env.cong _ i
-bindTermCong {a = a} env (Call' op ts) = a.algebra.semCong op (bindTermsCong env ts)
-
-bindTermsCong env                                    []        = []
-bindTermsCong env {tms = (_ :: _)} {tms' = (_ :: _)} (t :: ts) =
-  bindTermCong env t :: bindTermsCong env ts
+bindTermsCong env = bindTermsCong' env.cong
 
 public export
 bindHomo : (a : Algebra sig) -> (env : IFunction v a.setoid)