Use new notion of Fin to reduce casts.

6 files changed, 292 insertions, 195 deletions

diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr
index d70c8f3..dead052 100644
--- a/src/Data/Fin/Occurs.idr
+++ b/src/Data/Fin/Occurs.idr
@@ -1,114 +1,93 @@
 module Data.Fin.Occurs
 
 import Data.DPair
-import Data.Fin
+import Data.Fin.Strong
+import Data.Maybe
 import Data.Maybe.Properties
+import Data.Nat
 
--- Utilities -------------------------------------------------------------------
-
-predInjective : {n : Nat} -> pred n = S k -> n = S (S k)
-predInjective {n = S n} prf = cong S prf
-
-public export
-indexIsSuc : Fin n -> Exists (\k => n = S k)
-indexIsSuc FZ = Evidence _ Refl
-indexIsSuc (FS x) = Evidence _ Refl
-
-%inline %tcinline
-zero : (0 _ : Fin n) -> Fin n
-zero x = rewrite snd (indexIsSuc x) in FZ
-
-%inline %tcinline
-suc : (_ : Fin (pred n)) -> Fin n
-suc x =
-  replace {p = Fin}
-    (sym $ predInjective $ snd $ indexIsSuc x)
-    (FS $ rewrite sym $ snd $ indexIsSuc x in x)
+import Syntax.PreorderReasoning
 
 -- Thinning --------------------------------------------------------------------
 
 export
-thin : Fin n -> Fin (pred n) -> Fin n
-thin FZ y = FS y
+thin : SFin n -> SFin (pred n) -> SFin n
+thin FZ y = FS' y
 thin (FS x) FZ = FZ
 thin (FS x) (FS y) = FS (thin x y)
 
 -- Properties
 
 export
-thinInjective : (x : Fin n) -> {y, z : Fin (pred n)} -> thin x y = thin x z -> y = z
-thinInjective FZ prf = injective prf
+thinInjective : (x : SFin n) -> {y, z : SFin (pred n)} -> thin x y = thin x z -> y = z
+thinInjective FZ prf = injective {f = FS'} prf
 thinInjective (FS x) {y = FZ, z = FZ} prf = Refl
 thinInjective (FS x) {y = FS y, z = FS z} prf = cong FS $ thinInjective x $ injective prf
 
 export
-thinSkips : (x : Fin n) -> (y : Fin (pred n)) -> Not (thin x y = x)
+thinSkips : (x : SFin n) -> (y : SFin (pred n)) -> Not (thin x y = x)
+thinSkips FZ y prf = sucNonZero y prf
 thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf)
 
-%inline
-thinSucZero : (x : Fin n) -> thin (FS x) (zero x) = FZ
-thinSucZero x = rewrite snd (indexIsSuc x) in Refl
-
-%inline
-thinSucSuc : (x : Fin n) -> (z : Fin (pred n)) -> thin (FS x) (suc z) = FS (thin x z)
-thinSucSuc FZ FZ = Refl
-thinSucSuc FZ (FS z) = Refl
-thinSucSuc (FS x) FZ = Refl
-thinSucSuc (FS x) (FS z) = Refl
+thinSuc : {n : Nat} -> (x : SFin (S n)) -> (y : SFin n) -> thin (FS x) (FS' y) = FS (thin x y)
+thinSuc {n = S n} x y = rewrite sucIsFS y in Refl
 
 export
-thinInverse : (x, y : Fin n) -> (0 _ : Not (x = y)) -> (z ** thin x z = y)
+thinInverse : (x, y : SFin n) -> (0 _ : Not (x = y)) -> (z ** thin x z = y)
 thinInverse FZ FZ neq = void (neq Refl)
-thinInverse FZ (FS y) neq = (y ** Refl)
-thinInverse (FS x) FZ neq = (zero x ** thinSucZero x)
+thinInverse FZ (FS y) neq = (y ** sucIsFS y)
+thinInverse (FS x) FZ neq = (FZ ** Refl)
 thinInverse (FS x) (FS y) neq =
-  let (z ** prf) = thinInverse x y (neq . cong FS) in
-  (suc z ** trans (thinSucSuc x z) (cong FS prf))
+  let (z ** prf) = thinInverse x y (\prf => neq $ cong FS prf) in
+  (FS' z ** trans (thinSuc x z) (cong FS $ prf))
 
 -- Thickening ------------------------------------------------------------------
 
 export
-thick : Fin n -> Fin n -> Maybe (Fin (pred n))
+thick : SFin n -> SFin n -> Maybe (SFin (pred n))
 thick FZ FZ = Nothing
 thick FZ (FS y) = Just y
-thick (FS x) FZ = Just (zero x)
-thick (FS x) (FS y) = suc <$> thick x y
+thick (FS x) FZ = Just FZ
+thick (FS x) (FS y) = FS' <$> thick x y
 
 export
-thickRefl : (x : Fin n) -> IsNothing (thick x x)
+thickRefl : (x : SFin n) -> IsNothing (thick x x)
 thickRefl FZ = ItIsNothing
-thickRefl (FS x) = mapNothing suc (thickRefl x)
+thickRefl (FS x) = mapNothing FS' (thickRefl x)
 
 export
-thickNeq : (x, y : Fin n) -> (0 _ : Not (x = y)) -> IsJust (thick x y)
+thickNeq : (x, y : SFin n) -> (0 _ : Not (x = y)) -> IsJust (thick x y)
 thickNeq FZ FZ neq = void (neq Refl)
 thickNeq FZ (FS y) neq = ItIsJust
 thickNeq (FS x) FZ neq = ItIsJust
-thickNeq (FS x) (FS y) neq = mapIsJust suc (thickNeq x y (neq . cong FS))
+thickNeq (FS x) (FS y) neq = mapIsJust FS' (thickNeq x y (\prf => neq $ cong FS prf))
 
 export
-thickNothing : (x, y : Fin n) -> (0 _ : IsNothing (thick x y)) -> x = y
+thickNothing : (x, y : SFin n) -> (0 _ : IsNothing (thick x y)) -> x = y
 thickNothing FZ FZ prf = Refl
 thickNothing (FS x) (FS y) prf =
-  rewrite thickNothing x y (mapNothingInverse suc (thick x y) prf) in
-  Refl
+  cong FS (thickNothing x y (mapNothingInverse FS' (thick x y) prf))
 
-export
-thickJust : (x, y : Fin n) -> (0 _ : thick x y = Just z) -> thin x z = y
-thickJust FZ (FS y) Refl = Refl
-thickJust (FS x) FZ Refl = thinSucZero x
+export thickJust : (x : SFin n) -> (y : SFin n) -> (0 _ : thick x y = Just z) -> thin x z = y
+thickJust FZ (FS y) Refl = sucIsFS y
+thickJust (FS x) FZ Refl = Refl
 thickJust (FS x) (FS y) prf =
-  let 0 z = mapJustInverse suc (thick x y) prf in
-  rewrite snd $ z.snd in
-  trans (thinSucSuc x z.fst) (cong FS $ thickJust x y (fst $ z.snd))
+  let invertJust = mapJustInverse FS' (thick x y) prf in
+  Calc $
+    |~ thin (FS x) z
+    ~~ thin (FS x) (FS' invertJust.fst) ...(cong (thin (FS x)) $ snd invertJust.snd)
+    ~~ FS (thin x invertJust.fst)       ...(thinSuc x invertJust.fst)
+    ~~ FS y                             ...(cong FS $ thickJust x y (fst invertJust.snd))
 
 export
-thickThin : (x : Fin n) -> (y : Fin (pred n)) -> thick x (thin x y) = Just y
+thickThin : (x : SFin n) -> (y : SFin (pred n)) -> thick x (thin x y) = Just y
 thickThin x y =
-  let neq = thinSkips x y in
-  let isJust = thickNeq x (thin x y) (\prf => neq $ sym prf) in
-  let zPrf = extractIsJust isJust in
-  let z = zPrf.fst in
-  let 0 prf1 = zPrf.snd in
-  let 0 prf2 = thickJust x (thin x y) prf1 in
-  trans prf1 (cong Just $ thinInjective x prf2)
+  let
+    fromJust =
+      extractIsJust $
+      thickNeq x (thin x y) (\prf => thinSkips x y $ sym prf)
+  in
+  Calc $
+    |~ thick x (thin x y)
+    ~~ Just fromJust.fst  ...(fromJust.snd)
+    ~~ Just y             ...(cong Just $ thinInjective x $ thickJust x (thin x y) fromJust.snd)
diff --git a/src/Data/Fin/Strong.idr b/src/Data/Fin/Strong.idr
new file mode 100644
index 0000000..ebf3483
--- /dev/null
+++ b/src/Data/Fin/Strong.idr
@@ -0,0 +1,76 @@
+module Data.Fin.Strong
+
+import Data.Fin
+
+public export
+data SFin : Nat -> Type where
+  FZ : SFin (S n)
+  FS : SFin (S n) -> SFin (S (S n))
+
+public export
+0 indexPred : (0 x : Fin n) -> Nat
+indexPred {n = S n} x = n
+
+public export
+0 indexPredPrf : (0 x : Fin n) -> n = S (indexPred x)
+indexPredPrf {n = S n} x = Refl
+
+public export
+0 indexPred' : (0 x : SFin n) -> Nat
+indexPred' {n = S n} x = n
+
+public export
+0 indexPred'Prf : (0 x : SFin n) -> n = S (indexPred' x)
+indexPred'Prf {n = S n} x = Refl
+
+public export
+finToStrong : Fin n -> SFin n
+finToStrong FZ = FZ
+finToStrong (FS x) =
+  rewrite indexPredPrf x in
+  FS (replace {p = SFin} (indexPredPrf x) (finToStrong x))
+
+public export
+strongToFin : SFin n -> Fin n
+strongToFin FZ = FZ
+strongToFin (FS x) = FS (strongToFin x)
+
+export
+finToStrongToFin : (x : Fin n) -> strongToFin (finToStrong x) = x
+finToStrongToFin FZ = Refl
+finToStrongToFin (FS FZ) = Refl
+finToStrongToFin (FS (FS x)) = cong FS $ finToStrongToFin (FS x)
+
+export
+strongToFinToStrong : (x : SFin n) -> finToStrong (strongToFin x) = x
+strongToFinToStrong FZ = Refl
+strongToFinToStrong (FS x) = cong FS (strongToFinToStrong x)
+
+%inline
+export
+FS' : SFin n -> SFin (S n)
+FS' = finToStrong . FS . strongToFin
+
+export
+Injective (FS {n}) where
+  injective Refl = Refl
+
+export
+Injective (FS' {n}) where
+  injective {x = FZ, y = FZ} prf = Refl
+  injective {x = FS x, y = FS y} prf = cong FS $ injective {f = FS'} $ injective prf
+
+export
+Uninhabited (SFin 0) where uninhabited x impossible
+
+export
+Uninhabited (Strong.FS x = FZ) where uninhabited prf impossible
+
+export
+sucNonZero : (x : SFin n) -> Not (FS' x = FZ)
+sucNonZero FZ prf = absurd prf
+sucNonZero (FS x) prf = absurd prf
+
+export
+sucIsFS : (x : SFin (S n)) -> FS' x = FS x
+sucIsFS x = rewrite strongToFinToStrong x in Refl
diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 3b16f38..4b0ac3e 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -1,6 +1,7 @@
 module Data.Term
 
 import public Data.Vect
+import public Data.Fin.Strong
 import Data.Vect.Properties.Map
 import Syntax.PreorderReasoning
 
@@ -16,30 +17,38 @@ record Signature where
 
 public export
 data Term : Signature -> Nat -> Type where
-  Var : Fin n -> Term sig n
+  Var : SFin (S n) -> Term sig (S 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
+
 -- Substitution ----------------------------------------------------------------
 
 export
-pure : (Fin k -> Fin n) -> Fin k -> Term sig n
-pure r = Var . r
+pure : (SFin k -> SFin n) -> SFin k -> Term sig n
+pure r = Var' . r
 
 export
-(<$>) : (Fin k -> Term sig n) -> Term sig k -> Term sig n
+(<$>) : (SFin 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 (Fin k -> Term sig n)
-f .=. g = (i : Fin k) -> f i = g i
+0 (.=.) : Rel (SFin k -> Term sig n)
+f .=. g = (i : SFin 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 : {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) =
   cong (Op op) $
@@ -48,23 +57,23 @@ subCong prf (Op op ts) =
 -- Substitution is Monadic -----------------------------------------------------
 
 export
-(.) : (Fin k -> Term sig n) -> (Fin j -> Term sig k) -> Fin j -> Term sig n
+(.) : (SFin k -> Term sig n) -> (SFin j -> Term sig k) -> SFin 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 : Fin k -> Term sig n) ->
-  (g : Fin j -> Term sig k) ->
+  (f : SFin k -> Term sig n) ->
+  (g : SFin j -> Term sig k) ->
   (t : Term sig j) ->
   (f . g) <$> t = f <$> g <$> t
 subAssoc f g (Var i) = Refl
@@ -75,8 +84,8 @@ subAssoc f g (Op op ts) = cong (Op op) $ Calc $
 
 export
 subComp :
-  (f : Fin k -> Term sig n) ->
-  (r : Fin j -> Fin k) ->
+  (f : SFin (S k) -> Term sig n) ->
+  (r : SFin j -> SFin (S k)) ->
   f . pure r .=. f . r
 subComp f r i = Refl
 
diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index 2435c98..d65d185 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -13,8 +13,8 @@ import Syntax.PreorderReasoning
 public export
 record Property (sig : Signature) (k : Nat) where
   constructor MkProp
-  0 Prop : forall n. (Fin k -> Term sig n) -> Type
-  cong : forall n. {f, g : Fin k -> Term sig n} -> f .=. g -> Prop f -> Prop g
+  0 Prop : forall n. (SFin k -> Term sig n) -> Type
+  cong : forall n. {f, g : SFin k -> Term sig n} -> f .=. g -> Prop f -> Prop g
 
 %name Property p, q
 
@@ -39,7 +39,7 @@ All ps = MkProp (\f => All (\p => p.Prop f) ps) (\cong => mapRel (\p => p.cong c
 
 public export 0
 (<=>) : Property sig k -> Property sig k -> Type
-p <=> q = forall n. (f : Fin k -> Term sig n) -> p.Prop f <=> q.Prop f
+p <=> q = forall n. (f : SFin k -> Term sig n) -> p.Prop f <=> q.Prop f
 
 -- Properties
 
@@ -81,7 +81,7 @@ unifiesOp f = MkEquivalence
 
 public export 0
 Nothing : Property sig k -> Type
-Nothing p = forall n. (f : Fin k -> Term sig n) -> Not (p.Prop f)
+Nothing p = forall n. (f : SFin k -> Term sig n) -> Not (p.Prop f)
 
 -- Properties
 
@@ -92,7 +92,7 @@ nothingEquiv eq absurd f x = absurd f ((eq f).rightToLeft x)
 -- Extensions ------------------------------------------------------------------
 
 public export
-Extension : Property sig k -> (Fin k -> Term sig n) -> Property sig n
+Extension : Property sig k -> (SFin k -> Term sig n) -> Property sig n
 Extension p f = MkProp
   { Prop = \g => p.Prop (g . f)
   , cong = \prf => p.cong (\i => subCong prf (f i))
@@ -105,14 +105,14 @@ nothingExtends : Nothing p -> Nothing (Extension p f)
 nothingExtends absurd g x = void $ absurd (g . f) x
 
 export
-extendUnit : (p : Property sig k) -> p <=> Extension p Var
+extendUnit : (p : Property sig k) -> p <=> Extension p Var'
 extendUnit p f = MkEquivalence id id
 
 export
 extendAssoc :
   (p : Property sig j) ->
-  (f : Fin j -> Term sig k) ->
-  (g : Fin k -> Term sig m) ->
+  (f : SFin j -> Term sig k) ->
+  (g : SFin k -> Term sig m) ->
   Extension (Extension p f) g <=> Extension p (g . f)
 extendAssoc p f g h =
   MkEquivalence
@@ -122,8 +122,8 @@ extendAssoc p f g h =
 export
 extendUnify :
   (t, u : Term sig j) ->
-  (f : Fin j -> Term sig k) ->
-  (g : Fin k -> Term sig m) ->
+  (f : SFin j -> Term sig k) ->
+  (g : SFin k -> Term sig m) ->
   Extension (Unifies t u) (g . f) <=> Extension (Unifies (f <$> t) (f <$> u)) g
 extendUnify t u f g h =
   MkEquivalence
@@ -145,9 +145,9 @@ extendUnify t u f g h =
 -- Ordering --------------------------------------------------------------------
 
 public export
-record (<=) (f : Fin k -> Term sig m) (g : Fin k -> Term sig n) where
+record (<=) (f : SFin k -> Term sig m) (g : SFin k -> Term sig n) where
   constructor MkLte
-  sub : Fin n -> Term sig m
+  sub : SFin n -> Term sig m
   prf : f .=. sub . g
 
 %name Property.(<=) prf
@@ -166,8 +166,8 @@ lteCong prf1 prf2 prf3 = MkLte
   }
 
 export
-Reflexive (Fin k -> Term sig m) (<=) where
-  reflexive = MkLte Var (\i => sym $ subUnit _)
+Reflexive (SFin k -> Term sig m) (<=) where
+  reflexive = MkLte Var' (\i => sym $ subUnit _)
 
 export
 transitive : f <= g -> g <= h -> f <= h
@@ -181,11 +181,11 @@ transitive prf1 prf2 = MkLte
   }
 
 export
-varMax : (f : Fin k -> Term sig m) -> f <= Var
+varMax : (f : SFin k -> Term sig m) -> f <= Var'
 varMax f = MkLte f (\i => Refl)
 
 export
-compLte : f <= g -> (h : Fin k -> Term sig m) -> f . h <= g . h
+compLte : f <= g -> (h : SFin k -> Term sig m) -> f . h <= g . h
 compLte prf h = MkLte
   { sub = prf.sub
   , prf = \i => Calc $
@@ -197,8 +197,8 @@ compLte prf h = MkLte
 export
 lteExtend : 
   {p : Property sig k} ->
-  {f : Fin k -> Term sig m} ->
-  {g : Fin k -> Term sig n} ->
+  {f : SFin k -> Term sig m} ->
+  {g : SFin k -> Term sig n} ->
   (prf : f <= g) -> 
   p.Prop f -> 
   (Extension p g).Prop prf.sub
@@ -209,7 +209,7 @@ lteExtend prf x = p.cong prf.prf x
 public export
 Max : Property sig k -> Property sig k
 Max p = MkProp
-  { Prop = \f => (p.Prop f, forall n. (g : Fin k -> Term sig n) -> p.Prop g -> g <= f)
+  { Prop = \f => (p.Prop f, forall n. (g : SFin k -> Term sig n) -> p.Prop g -> g <= f)
   , cong = \cong, (x, max) => (p.cong cong x, \g, y => lteCong (\_ => Refl) cong (max g y))
   }
 
@@ -226,8 +226,8 @@ public export 0
 DClosed : Property sig k -> Type
 DClosed p =
   forall m, n.
-  (f : Fin k -> Term sig m) ->
-  (g : Fin k -> Term sig n) ->
+  (f : SFin k -> Term sig m) ->
+  (g : SFin k -> Term sig n) ->
   f <= g ->
   p.Prop g ->
   p.Prop f
@@ -245,9 +245,9 @@ unifiesDClosed t u f g prf1 prf2 = Calc $
 
 optimistLemma :
   {q : Property sig j} ->
-  {a : Fin j -> Term sig k} ->
-  {f : Fin k -> Term sig m} ->
-  {g : Fin m -> Term sig n} ->
+  {a : SFin j -> Term sig k} ->
+  {f : SFin k -> Term sig m} ->
+  {g : SFin m -> Term sig n} ->
   DClosed p ->
   (Max (Extension p a)).Prop f ->
   (Max (Extension q (f . a))).Prop g ->
diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index 2955aa2..7cb01d6 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -2,6 +2,7 @@ module Data.Term.Unify
 
 import Data.DPair
 import Data.Fin.Occurs
+import Data.Fin.Strong
 import Data.Maybe.Properties
 import Data.Term
 import Data.Term.Zipper
@@ -13,10 +14,10 @@ import Syntax.PreorderReasoning
 -- Check -----------------------------------------------------------------------
 
 export
-check : Fin k -> Term sig k -> Maybe (Term sig (pred k))
-checkAll : Fin k -> Vect n (Term sig k) -> Maybe (Vect n (Term sig (pred k)))
+check : SFin k -> Term sig k -> Maybe (Term sig (pred k))
+checkAll : SFin k -> Vect n (Term sig k) -> Maybe (Vect n (Term sig (pred k)))
 
-check x (Var y) = Var <$> thick x y
+check x (Var y) = Var' <$> thick x y
 check x (Op op ts) = Op op <$> checkAll x ts
 
 checkAll x [] = Just []
@@ -25,15 +26,18 @@ checkAll x (t :: ts) = [| check x t :: checkAll x ts |]
 -- Properties
 
 export
-checkOccurs : (x : Fin k) -> (zip : Zipper sig k) -> IsNothing (check x (zip + Var x))
+checkOccurs :
+  (x : SFin k) ->
+  (zip : Zipper sig k) ->
+  IsNothing (check x (zip + Var' x))
 checkAllOccurs :
-  (x : Fin k) ->
-  (i : Fin (S n)) ->
-  (ts : Vect n (Term sig k)) ->
+  (x : SFin k) ->
+  (i : SFin n) ->
+  (ts : Vect (pred n) (Term sig k)) ->
   (zip : Zipper sig k) ->
-  IsNothing (checkAll x (insertAt i (zip + Var x) ts))
+  IsNothing (checkAll x (insertAt' i (zip + Var' x) ts))
 
-checkOccurs x Top = mapNothing Var (thickRefl x)
+checkOccurs x Top = mapNothing Var' (thickRefl x)
 checkOccurs x (Op op i ts zip) = mapNothing (Op op) (checkAllOccurs x i ts zip)
 
 checkAllOccurs x FZ ts zip =
@@ -47,19 +51,19 @@ checkAllOccurs x (FS i) (t :: ts) zip =
 
 export
 checkNothing :
-  (x : Fin k) ->
+  (x : SFin k) ->
   (t : Term sig k) ->
   (0 _ : IsNothing (check x t)) ->
-  (zip : Zipper sig k ** t = zip + Var x)
+  (zip : Zipper sig k ** t = zip + Var' x)
 checkAllNothing :
-  (x : Fin k) ->
+  (x : SFin k) ->
   (t : Term sig k) ->
   (ts : Vect n (Term sig k)) ->
   (0 _ : IsNothing (checkAll x (t :: ts))) ->
-  (i ** ts' ** zip : Zipper sig k ** t :: ts = insertAt i (zip + Var x) ts')
+  (i ** ts' ** zip : Zipper sig k ** t :: ts = insertAt' i (zip + Var' x) ts')
 
 checkNothing x (Var y) prf =
-  (Top ** sym (cong Var (thickNothing x y (mapNothingInverse Var (thick x y) prf))))
+  (Top ** sym (cong Var (thickNothing x y (mapNothingInverse Var' (thick x y) prf))))
 checkNothing x (Op op (t :: ts)) prf =
   let (i ** ts' ** zip ** prf) = checkAllNothing x t ts (mapNothingInverse (Op op) _ prf) in
   (Op op i ts' zip ** cong (Op op) prf)
@@ -74,13 +78,18 @@ checkAllNothing x t ts prf with (appNothingInverse (Just (::) <*> check x t) (ch
     (FS i ** t :: ts ** zip ** cong (t ::) prf)
 
 export
-checkThin : (x : Fin k) -> (t : Term sig (pred k)) -> IsJust (check x (pure (thin x) <$> t))
+checkThin :
+  (x : SFin (S k)) ->
+  (t : Term sig k) ->
+  IsJust (check x (pure (thin x) <$> t))
 checkAllThin :
-  (x : Fin k) ->
-  (ts : Vect n (Term sig (pred k))) ->
+  (x : SFin (S k)) ->
+  (ts : Vect n (Term sig k)) ->
   IsJust (checkAll x (map (pure (thin x) <$>) ts))
 
-checkThin x (Var y) = mapIsJust Var (thickNeq x (thin x y) (\prf => thinSkips x y $ sym prf))
+checkThin x (Var y) =
+  mapIsJust Var' $
+  thickNeq x (thin x y) (\prf => thinSkips x y $ sym prf)
 checkThin x (Op op ts) = mapIsJust (Op op) (checkAllThin x ts)
 
 checkAllThin x [] = ItIsJust
@@ -91,23 +100,23 @@ checkAllThin x (t :: ts) =
 
 export
 checkJust :
-  (x : Fin k) ->
+  (x : SFin k) ->
   (t : Term sig k) ->
   (0 _ : check x t = Just u) ->
   t = pure (thin x) <$> u
 checkAllJust :
-  (x : Fin k) ->
+  (x : SFin k) ->
   (ts : Vect n (Term sig k)) ->
   (0 _ : checkAll x ts = Just us) ->
   ts = map (pure (thin x) <$>) us
 
 checkJust x (Var y) prf =
-  let 0 z = mapJustInverse Var (thick x y) prf in
+  let 0 z = mapJustInverse Var' (thick x y) prf in
   let 0 prf = thickJust x y (fst z.snd) in
   sym $ Calc $
     |~ pure (thin x) <$> u
-    ~~ pure (thin x) <$> Var z.fst ...(cong (pure (thin x) <$>) $ snd z.snd)
-    ~~ Var y                       ...(cong Var prf)
+    ~~ pure (thin x) <$> Var' z.fst ...(cong (pure (thin x) <$>) $ snd z.snd)
+    ~~ Var' y                       ...(cong Var' prf)
 checkJust x (Op op ts) prf =
   let 0 z = mapJustInverse (Op op) (checkAll x ts) prf in
   let 0 prf = checkAllJust x ts (fst z.snd) in
@@ -130,44 +139,47 @@ checkAllJust x (t :: ts) prf =
 -- Single Variable Substitution ------------------------------------------------
 
 export
-for : Term sig (pred k) -> Fin k -> Fin k -> Term sig (pred k)
-(t `for` x) y = maybe t Var (thick x y)
+for : Term sig (pred k) -> SFin k -> SFin k -> Term sig (pred k)
+(t `for` x) y = maybe t Var' (thick x y)
 
 export
-forThin : (0 t : Term sig (pred k)) -> (x : Fin k) -> (t `for` x) . thin x .=. Var
-forThin t x i = cong (maybe t Var) (thickThin x i)
+forThin :
+  (0 t : Term sig (pred k)) ->
+  (x : SFin k) ->
+  (t `for` x) . thin x .=. Var'
+forThin t x i = cong (maybe t Var') (thickThin x i)
 
 export
 forUnifies :
-  (x : Fin k) ->
+  (x : SFin k) ->
   (t : Term sig k) ->
   (0 _ : check x t = Just u) ->
-  (u `for` x) <$> t = (u `for` x) <$> Var x
+  (u `for` x) <$> t = (u `for` x) <$> Var' x
 forUnifies x t prf = Calc $
   |~ (u `for` x) <$> t
   ~~ (u `for` x) <$> pure (thin x) <$> u ...(cong ((u `for` x) <$>) $ checkJust x t prf)
   ~~ (u `for` x) . thin x <$> u          ...(sym $ subAssoc (u `for` x) (pure (thin x)) u)
-  ~~ Var <$> u                           ...(subCong (forThin u x) u)
+  ~~ Var' <$> u                          ...(subCong (forThin u x) u)
   ~~ u                                   ...(subUnit u)
-  ~~ (u `for` x) <$> Var x               ...(sym $ cong (maybe u Var) $ extractIsNothing $ thickRefl x)
+  ~~ (u `for` x) <$> Var' x              ...(sym $ cong (maybe u Var') $ extractIsNothing $ thickRefl x)
 
 -- Substitution List -----------------------------------------------------------
 
 public export
 data AList : Signature -> Nat -> Nat -> Type where
   Lin : AList sig n n
-  (:<) : AList sig k n -> (Term sig k, Fin (S k)) -> AList sig (S k) n
+  (:<) : AList sig k n -> (Term sig k, SFin (S k)) -> AList sig (S k) n
 
 %name AList sub
 
 namespace Exists
   public export
-  (:<) : Exists (AList sig n) -> (Term sig n, Fin (S n)) -> Exists (AList sig (S n))
+  (:<) : Exists (AList sig n) -> (Term sig n, SFin (S n)) -> Exists (AList sig (S n))
   Evidence _ sub :< tx = Evidence _ (sub :< tx)
 
 export
-eval : AList sig k n -> Fin k -> Term sig n
-eval [<] = Var
+eval : AList sig k n -> SFin k -> Term sig n
+eval [<] = Var'
 eval (sub :< (t, x)) = eval sub . (t `for` x)
 
 export
@@ -190,28 +202,15 @@ evalHomo sub2 (sub1 :< (t, x)) i = Calc $
 
 -- Unification -----------------------------------------------------------------
 
-flexFlex : (x, y : Fin n) -> Exists (AList sig n)
-flexFlex x y =
-  rewrite (snd $ indexIsSuc x) in
-  case thick x' y' of
-    Just z => Evidence _ [<(Var z, x')]
-    Nothing => Evidence _ [<]
-  where
-  x', y' : Fin (S $ fst $ indexIsSuc x)
-  x' = replace {p = Fin} (snd $ indexIsSuc x) x
-  y' = replace {p = Fin} (snd $ indexIsSuc x) y
-
-flexRigid : Fin n -> Term sig n -> Maybe (Exists (AList sig n))
-flexRigid x t =
-  rewrite (snd $ indexIsSuc x) in
-  case check x' t' of
-    Just u => Just (Evidence _ [<(u, x')])
-    Nothing => Nothing
-  where
-  x' : Fin (S $ fst $ indexIsSuc x)
-  x' = replace {p = Fin} (snd $ indexIsSuc x) x
-  t' : Term sig (S $ fst $ indexIsSuc x)
-  t' = replace {p = Term sig} (snd $ indexIsSuc x) t
+flexFlex : (x : SFin (S n)) -> (y : SFin (S n)) -> Exists (AList sig (S n))
+flexFlex x y = case thick x y of
+  Just z => Evidence _ [<(Var' z, x)]
+  Nothing => Evidence _ [<]
+
+flexRigid : SFin (S n) -> Term sig (S n) -> Maybe (Exists (AList sig (S n)))
+flexRigid x t = case check x t of
+  Just u => Just (Evidence _ [<(u, x)])
+  Nothing => Nothing
 
 export
 amgu :
diff --git a/src/Data/Term/Zipper.idr b/src/Data/Term/Zipper.idr
index 3f6668a..608e86c 100644
--- a/src/Data/Term/Zipper.idr
+++ b/src/Data/Term/Zipper.idr
@@ -2,17 +2,53 @@ module Data.Term.Zipper
 
 import Data.DPair
 import Data.Fin.Occurs
-import Data.Vect.Properties.Insert
+import Data.Fin.Strong
 import Data.Vect.Properties.Map
 import Data.Term
 import Syntax.PreorderReasoning
 
+-- Utilities -------------------------------------------------------------------
+
+public export
+insertAt' : SFin k -> a -> Vect (pred k) a -> Vect k a
+insertAt' FZ x xs = x :: xs
+insertAt' (FS i) x (y :: xs) = y :: insertAt' i x xs
+
+public export
+deleteAt' : SFin k -> Vect k a -> Vect (pred k) a
+deleteAt' FZ (x :: xs) = xs
+deleteAt' (FS i) (x :: xs) = x :: deleteAt' i xs
+
+mapInsertAt :
+  (0 f : a -> b) ->
+  (i : SFin k) ->
+  (x : a) ->
+  (xs : Vect (pred k) a) ->
+  map f (insertAt' i x xs) = insertAt' i (f x) (map f xs)
+mapInsertAt f FZ x xs = Refl
+mapInsertAt f (FS i) x (y :: xs) = cong (f y ::) $ mapInsertAt f i x xs
+
+insertAtDeleteAt :
+  (i : SFin k) ->
+  (xs : Vect k a) ->
+  insertAt' i (index (strongToFin i) xs) (deleteAt' i xs) = xs
+insertAtDeleteAt FZ (x :: xs) = Refl
+insertAtDeleteAt (FS i) (x :: xs) = cong (x ::) $ insertAtDeleteAt i xs
+
+indexInsertAt :
+  (i : SFin k) ->
+  (x : a) ->
+  (xs : Vect (pred k) a) ->
+  index (strongToFin i) (insertAt' i x xs) = x
+indexInsertAt FZ x xs = Refl
+indexInsertAt (FS i) x (y :: xs) = indexInsertAt i x xs
+
 -- Definition ------------------------------------------------------------------
 
 public export
 data Zipper : Signature -> Nat -> Type where
   Top : Zipper sig n
-  Op : sig.Operator (S k) -> Fin (S k) -> Vect k (Term sig n) -> Zipper sig n -> Zipper sig n
+  Op : sig.Operator k -> SFin k -> Vect (pred k) (Term sig n) -> Zipper sig n -> Zipper sig n
 
 %name Zipper zip
 
@@ -45,7 +81,7 @@ assoc (Op op i ts zip1) zip2 zip3 = cong (Op op i ts) (assoc zip1 zip2 zip3)
 public export
 (+) : Zipper sig n -> Term sig n -> Term sig n
 Top + t = t
-Op op i ts zip + t = Op op (insertAt i (zip + t) ts)
+Op op i ts zip + t = Op op (insertAt' i (zip + t) ts)
 
 -- Properties
 
@@ -56,12 +92,12 @@ actionAssoc :
   (zip1 ++ zip2) + t = zip1 + (zip2 + t)
 actionAssoc Top zip2 t = Refl
 actionAssoc (Op op i ts zip1) zip2 t =
-  cong (\t => Op op (insertAt i t ts)) $ actionAssoc zip1 zip2 t
+  cong (\t => Op op (insertAt' i t ts)) $ actionAssoc zip1 zip2 t
 
 -- Substitution ----------------------------------------------------------------
 
 export
-(<$>) : (Fin k -> Term sig n) -> Zipper sig k -> Zipper sig n
+(<$>) : (SFin k -> Term sig n) -> Zipper sig k -> Zipper sig n
 f <$> Top = Top
 f <$> Op op i ts zip = Op op i (map (f <$>) ts) (f <$> zip)
 
@@ -69,35 +105,27 @@ f <$> Op op i ts zip = Op op i (map (f <$>) ts) (f <$> zip)
 
 export
 actionHomo :
-  (0 f : Fin k -> Term sig n) ->
+  (0 f : SFin k -> Term sig n) ->
   (zip : Zipper sig k) ->
   (0 t : Term sig k) ->
   f <$> zip + t = (f <$> zip) + (f <$> t)
 actionHomo f Top t = Refl
 actionHomo f (Op op i ts zip) t = cong (Op op) $ Calc $
-  |~ map (f <$>) (insertAt i (zip + t) ts)
-  ~~ insertAt i (f <$> zip + t) (map (f <$>) ts)           ...(mapInsertAt (f <$>) i (zip + t) ts)
-  ~~ insertAt i ((f <$> zip) + (f <$> t)) (map (f <$>) ts) ...(cong (\t => insertAt i t (map (f <$>) ts)) $ actionHomo f zip t)
+  |~ map (f <$>) (insertAt' i (zip + t) ts)
+  ~~ insertAt' i (f <$> zip + t) (map (f <$>) ts)           ...(mapInsertAt (f <$>) i (zip + t) ts)
+  ~~ insertAt' i ((f <$> zip) + (f <$> t)) (map (f <$>) ts) ...(cong (\t => insertAt' i t (map (f <$>) ts)) $ actionHomo f zip t)
 
 -- Cycles ----------------------------------------------------------------------
 
-pivotAt : sig.Operator k -> Fin k -> Vect k (Term sig n) -> Zipper sig n
-pivotAt op i ts =
-  let op' = replace {p = sig.Operator} (snd prf) op in
-  let i' = replace {p = Fin} (snd prf) i in
-  let ts' = replace {p = flip Vect (Term sig n)} (snd prf) ts in
-  Op op' i' (deleteAt i' ts') Top
-  where
-  prf : Exists (\j => k = S j)
-  prf = indexIsSuc i
+pivotAt : sig.Operator k -> SFin k -> Vect k (Term sig n) -> Zipper sig n
+pivotAt op i ts = Op op i (deleteAt' i ts) Top
 
 actionPivotAt :
   (op : sig.Operator k) ->
-  (i : Fin k) ->
+  (i : SFin k) ->
   (ts : Vect k (Term sig n)) ->
-  pivotAt op i ts + index i ts = Op op ts
-actionPivotAt op i@FZ ts = cong (Op op) $ insertAtIndex i ts
-actionPivotAt op i@(FS _) ts = cong (Op op) $ insertAtIndex i ts
+  pivotAt op i ts + index (strongToFin i) ts = Op op ts
+actionPivotAt op i ts = cong (Op op) $ insertAtDeleteAt i ts
 
 pivotNotTop : (zip : Zipper sig k) -> Not (zip ++ pivotAt op i ts = Top)
 pivotNotTop (Op op' j us zip) prf impossible
@@ -108,17 +136,23 @@ noCycles Top t prf = Refl
 noCycles (Op {k} op i ts zip') t@(Op {k = j} op' us) prf =
   void $ pivotNotTop zip' prf''
   where
-  I : Fin j
-  I = replace {p = Fin} (opInjectiveLen prf) i
+  i' : Fin k
+  i' = strongToFin i
+
+  I : SFin j
+  I = replace {p = SFin} (opInjectiveLen prf) i
+
+  I' : Fin j
+  I' = strongToFin I
 
-  prf' : ((zip' ++ pivotAt op' I us) + index I us = index I us)
+  prf' : ((zip' ++ pivotAt op' I us) + index I' us = index I' us)
   prf' = Calc $
-    |~ (zip' ++ pivotAt op' I us) + index I us
-    ~~ zip' + (pivotAt op' I us + index I us)      ...(actionAssoc zip' (pivotAt op' I us) (index I us))
-    ~~ zip' + Op op' us                            ...(cong (zip' +) $ actionPivotAt op' I us)
-    ~~ index i (insertAt i (zip' + Op op' us) ts)  ..<(indexInsertAt i (zip' + Op op' us) ts)
-    ~~ index i (rewrite opInjectiveLen prf in us)  ...(cong (index i) $ opInjectiveTs prf)
-    ~~ index I us                                  ...(rewrite opInjectiveLen prf in Refl)
+    |~ (zip' ++ pivotAt op' I us) + index I' us
+    ~~ zip' + (pivotAt op' I us + index I' us)      ...(actionAssoc zip' (pivotAt op' I us) (index I' us))
+    ~~ zip' + Op op' us                             ...(cong (zip' +) $ actionPivotAt op' I us)
+    ~~ index i' (insertAt' i (zip' + Op op' us) ts) ..<(indexInsertAt i (zip' + Op op' us) ts)
+    ~~ index i' (rewrite opInjectiveLen prf in us)  ...(cong (index i') $ opInjectiveTs prf)
+    ~~ index I' us                                  ...(rewrite opInjectiveLen prf in Refl)
 
   prf'' : zip' ++ pivotAt op' I us = Top
-  prf'' = noCycles (zip' ++ pivotAt op' I us) (assert_smaller t (index I us)) prf'
+  prf'' = noCycles (zip' ++ pivotAt op' I us) (assert_smaller t (index I' us)) prf'