Prove unification correct.

1 files changed, 12 insertions, 1 deletions

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index ebb7b00..b65859e 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -1,7 +1,8 @@
 module Data.Term
 
-import public Data.Vect
+import public Data.DPair
 import public Data.Fin.Strong
+import public Data.Vect
 import Data.Vect.Properties.Map
 import Syntax.PreorderReasoning
 
@@ -16,6 +17,10 @@ record Signature where
 %name Signature sig
 
 public export
+(.Op) : Signature -> Type
+sig .Op = Exists sig.Operator
+
+public export
 data Term : Signature -> Nat -> Type where
   Var : SFin (S n) -> Term sig (S n)
   Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n
@@ -99,6 +104,12 @@ opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
 opInjectiveLen Refl = Refl
 
 export
+opInjectiveOp :
+  (prf : Op {sig, k} op ts = Op {sig, k = n} op' us) ->
+  the sig.Op (Evidence k op) = Evidence n op'
+opInjectiveOp Refl = Refl
+
+export
 opInjectiveTs' : {0 ts, us : Vect k (Term sig n)} -> (prf : Op op ts = Op op us) -> ts = us
 opInjectiveTs' Refl = Refl