3 files changed, 146 insertions, 113 deletions

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'