1 files changed, 19 insertions, 28 deletions
diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 4bb787f..385b864 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -1,7 +1,6 @@
 module Data.Term
 
 import public Data.DPair
-import public Data.Fin.Strong
 import public Data.Vect
 import Data.Vect.Properties.Map
 import Syntax.PreorderReasoning
@@ -27,66 +26,58 @@ interface DecOp (0 sig : Signature) where
 
 public export
 data Term : Signature -> Nat -> Type where
-  Var : SFin (S n) -> Term sig (S n)
+  Var : Fin n -> Term sig n
   Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n
 
 %name Term t, u, v
 
 export
-Var' : SFin n -> Term sig n
-Var' x = rewrite indexPred'Prf x in Var (replace {p = SFin} (indexPred'Prf x) x)
-
-export
-varIsVar : (x : SFin (S n)) -> Var' x = Var x
-varIsVar x = Refl
-
-export
 Uninhabited (Op op ts = Var x) where uninhabited prf impossible
 
 -- Substitution ----------------------------------------------------------------
 
 export
-pure : (SFin k -> SFin n) -> SFin k -> Term sig n
-pure r = Var' . r
+pure : (Fin k -> Fin n) -> Fin k -> Term sig n
+pure r = Var . r
 
 public export
-(<$>) : (SFin k -> Term sig n) -> Term sig k -> Term sig n
+(<$>) : (Fin k -> Term sig n) -> Term sig k -> Term sig n
 f <$> Var i = f i
 f <$> Op op ts = Op op (map (\t => f <$> assert_smaller ts t) ts)
 
 -- Extensional Equality --------------------------------------------------------
 
 public export
-0 (.=.) : Rel (SFin k -> Term sig n)
-f .=. g = (i : SFin k) -> f i = g i
+0 (.=.) : Rel (Fin k -> Term sig n)
+f .=. g = (i : Fin k) -> f i = g i
 
 export
-subCong : {f, g : SFin 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) =
+subExtensional : {f, g : Fin k -> Term sig n} -> f .=. g -> (t : Term sig k) -> f <$> t = g <$> t
+subExtensional prf (Var i) = prf i
+subExtensional prf (Op op ts) =
   cong (Op op) $
-  mapExtensional (f <$>) (g <$>) (\t => subCong prf (assert_smaller ts t)) ts
+  mapExtensional (f <$>) (g <$>) (\t => subExtensional prf (assert_smaller ts t)) ts
 
 -- Substitution is Monadic -----------------------------------------------------
 
 public export
-(.) : (SFin k -> Term sig n) -> (SFin j -> Term sig k) -> SFin j -> Term sig n
+(.) : (Fin k -> Term sig n) -> (Fin j -> Term sig k) -> Fin j -> Term sig n
 f . g = (f <$>) . g
 
 -- Properties
 
 export
-subUnit : (t : Term sig n) -> Var' <$> t = t
+subUnit : (t : Term sig n) -> Var <$> t = t
 subUnit (Var i) = Refl
 subUnit (Op op ts) = cong (Op op) $ Calc $
-  |~ map (Var' <$>) ts
-  ~~ map id ts         ...(mapExtensional (Var' <$>) id (\t => subUnit (assert_smaller ts t)) ts)
-  ~~ ts                ...(mapId ts)
+  |~ map (Var <$>) ts
+  ~~ map id ts        ...(mapExtensional (Var <$>) id (\t => subUnit (assert_smaller ts t)) ts)
+  ~~ ts               ...(mapId ts)
 
 export
 subAssoc :
-  (f : SFin k -> Term sig n) ->
-  (g : SFin j -> Term sig k) ->
+  (f : Fin k -> Term sig n) ->
+  (g : Fin j -> Term sig k) ->
   (t : Term sig j) ->
   (f . g) <$> t = f <$> g <$> t
 subAssoc f g (Var i) = Refl
@@ -97,8 +88,8 @@ subAssoc f g (Op op ts) = cong (Op op) $ Calc $
 
 export
 subComp :
-  (f : SFin k -> Term sig n) ->
-  (r : SFin j -> SFin k) ->
+  (f : Fin k -> Term sig n) ->
+  (r : Fin j -> Fin k) ->
   f . pure r .=. f . r
 subComp f r i = Refl