Remove SFin.

Delete unused modules.

Restructure some proofs to reduce the number of lemmas.

3 files changed, 359 insertions, 427 deletions

diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index bed4e49..2de450f 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -15,8 +15,8 @@ import Syntax.PreorderReasoning
 public export
 record Property (sig : Signature) (k : Nat) where
   constructor MkProp
-  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
+  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
 
 %name Property p, q
 
@@ -28,9 +28,9 @@ Unifies t u = MkProp
   { Prop = \f => f <$> t = f <$> u
   , cong = \cong, prf => Calc $
     |~ _ <$> t
-    ~~ _ <$> t ..<(subCong cong t)
+    ~~ _ <$> t ..<(subExtensional cong t)
     ~~ _ <$> u ...(prf)
-    ~~ _ <$> u ...(subCong cong u)
+    ~~ _ <$> u ...(subExtensional cong u)
   }
 
 public export
@@ -46,8 +46,8 @@ UnifiesAll ts us = All (zipWith Unifies ts us)
 public export
 record (<=>) (p, q : Property sig k) where
   constructor MkEquivalence
-  leftToRight : forall n. (f : SFin k -> Term sig n) -> p.Prop f -> q.Prop f
-  rightToLeft : forall n. (f : SFin k -> Term sig n) -> q.Prop f -> p.Prop f
+  leftToRight : forall n. (f : Fin k -> Term sig n) -> p.Prop f -> q.Prop f
+  rightToLeft : forall n. (f : Fin k -> Term sig n) -> q.Prop f -> p.Prop f
 
 -- Properties
 
@@ -77,7 +77,7 @@ unifiesOp op ts us = MkEquivalence
   leftToRight :
     forall k.
     (ts, us : Vect k (Term sig j)) ->
-    (0 f : (SFin j -> Term sig n)) ->
+    (0 f : (Fin j -> Term sig n)) ->
     map (f <$>) ts = map (f <$>) us ->
     (UnifiesAll ts us).Prop f
   leftToRight [] [] f prf = []
@@ -87,7 +87,7 @@ unifiesOp op ts us = MkEquivalence
   rightToLeft :
     forall k.
     (ts, us : Vect k (Term sig j)) ->
-    (0 f : (SFin j -> Term sig n)) ->
+    (0 f : (Fin j -> Term sig n)) ->
     (UnifiesAll ts us).Prop f ->
     map (f <$>) ts = map (f <$>) us
   rightToLeft [] [] f [] = Refl
@@ -97,7 +97,7 @@ unifiesOp op ts us = MkEquivalence
 
 public export 0
 Nothing : Property sig k -> Type
-Nothing p = forall n. (f : SFin k -> Term sig n) -> Not (p.Prop f)
+Nothing p = forall n. (f : Fin k -> Term sig n) -> Not (p.Prop f)
 
 -- Properties
 
@@ -108,10 +108,10 @@ nothingEquiv eq absurd f x = absurd f (eq.rightToLeft f x)
 -- Extensions ------------------------------------------------------------------
 
 public export
-Extension : Property sig k -> (SFin k -> Term sig n) -> Property sig n
+Extension : Property sig k -> (Fin 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))
+  , cong = \prf => p.cong (\i => subExtensional prf (f i))
   }
 
 -- Properties
@@ -122,7 +122,7 @@ nothingExtends absurd g x = void $ absurd (g . f) x
 
 export
 extendCong2 :
-  {f, g : SFin n -> Term sig k} ->
+  {f, g : Fin n -> Term sig k} ->
   {p, q : Property sig n} ->
   f .=. g ->
   p <=> q ->
@@ -133,7 +133,7 @@ extendCong2 prf1 prf2 = MkEquivalence
 
 export
 extendCong :
-  (f : SFin n -> Term sig k) ->
+  (f : Fin n -> Term sig k) ->
   p <=> q ->
   Extension p f <=> Extension q f
 extendCong f prf = MkEquivalence
@@ -141,14 +141,14 @@ extendCong f prf = MkEquivalence
   (\g => prf.rightToLeft (g . f))
 
 export
-extendUnit : (p : Property sig k) -> p <=> Extension p Var'
+extendUnit : (p : Property sig k) -> p <=> Extension p Var
 extendUnit p = MkEquivalence (\_, x => x) (\_, x => x)
 
 export
 extendAssoc :
   (p : Property sig j) ->
-  (f : SFin j -> Term sig k) ->
-  (g : SFin k -> Term sig m) ->
+  (f : Fin j -> Term sig k) ->
+  (g : Fin k -> Term sig m) ->
   Extension (Extension p f) g <=> Extension p (g . f)
 extendAssoc p f g =
   MkEquivalence
@@ -158,31 +158,31 @@ extendAssoc p f g =
 export
 extendUnify :
   (t, u : Term sig j) ->
-  (f : SFin j -> Term sig k) ->
-  (g : SFin k -> Term sig m) ->
+  (f : Fin j -> Term sig k) ->
+  (g : Fin k -> Term sig m) ->
   Extension (Unifies t u) (g . f) <=> Extension (Unifies (f <$> t) (f <$> u)) g
 extendUnify t u f g =
   MkEquivalence
     (\h, prf => Calc $
       |~ (h . g) <$> (f <$> t)
       ~~ ((h . g) . f) <$> t   ...(sym $ subAssoc (h . g) f t)
-      ~~ (h . (g . f)) <$> t   ...(subCong (\i => subAssoc h g (f i)) t)
+      ~~ (h . (g . f)) <$> t   ...(subExtensional (\i => subAssoc h g (f i)) t)
       ~~ (h . (g . f)) <$> u   ...(prf)
-      ~~ ((h . g) . f) <$> u   ...(sym $ subCong (\i => subAssoc h g (f i)) u)
+      ~~ ((h . g) . f) <$> u   ...(sym $ subExtensional (\i => subAssoc h g (f i)) u)
       ~~ (h . g) <$> (f <$> u) ...(subAssoc (h . g) f u))
     (\h, prf => Calc $
       |~ (h . (g . f)) <$> t
-      ~~ ((h . g) . f) <$> t   ...(sym $ subCong (\i => subAssoc h g (f i)) t)
+      ~~ ((h . g) . f) <$> t   ...(sym $ subExtensional (\i => subAssoc h g (f i)) t)
       ~~ (h . g) <$> (f <$> t) ...(subAssoc (h . g) f t)
       ~~ (h . g) <$> (f <$> u) ...(prf)
       ~~ ((h . g) . f) <$> u   ...(sym $ subAssoc (h . g) f u)
-      ~~ (h . (g . f)) <$> u   ...(subCong (\i => subAssoc h g (f i)) u))
+      ~~ (h . (g . f)) <$> u   ...(subExtensional (\i => subAssoc h g (f i)) u))
 
 export
 extendUnifyAll :
   (ts, us : Vect n (Term sig j)) ->
-  (f : SFin j -> Term sig k) ->
-  (g : SFin k -> Term sig m) ->
+  (f : Fin j -> Term sig k) ->
+  (g : Fin k -> Term sig m) ->
   Extension (UnifiesAll ts us) (g . f) <=>
   Extension (UnifiesAll (map (f <$>) ts) (map (f <$>) us)) g
 extendUnifyAll [] [] f g = MkEquivalence (\h, [] => []) (\h, [] => [])
@@ -196,9 +196,9 @@ extendUnifyAll (t :: ts) (u :: us) f g =
 -- Ordering --------------------------------------------------------------------
 
 public export
-record (<=) (f : SFin k -> Term sig m) (g : SFin k -> Term sig n) where
+record (<=) (f : Fin k -> Term sig m) (g : Fin k -> Term sig n) where
   constructor MkLte
-  sub : SFin n -> Term sig m
+  sub : Fin n -> Term sig m
   prf : f .=. sub . g
 
 %name Property.(<=) prf
@@ -217,8 +217,8 @@ lteCong prf1 prf2 prf3 = MkLte
   }
 
 export
-Reflexive (SFin k -> Term sig m) (<=) where
-  reflexive = MkLte Var' (\i => sym $ subUnit _)
+Reflexive (Fin k -> Term sig m) (<=) where
+  reflexive = MkLte Var (\i => sym $ subUnit _)
 
 export
 transitive : f <= g -> g <= h -> f <= h
@@ -232,35 +232,38 @@ transitive prf1 prf2 = MkLte
   }
 
 export
-varMax : (f : SFin k -> Term sig m) -> f <= Var'
+varMax : (f : Fin k -> Term sig m) -> f <= Var
 varMax f = MkLte f (\i => Refl)
 
 export
-compLte : f <= g -> (h : SFin k -> Term sig m) -> f . h <= g . h
+compLte : f <= g -> (h : Fin k -> Term sig m) -> f . h <= g . h
 compLte prf h = MkLte
   { sub = prf.sub
   , prf = \i => Calc $
     |~ f <$> h i
-    ~~ (prf.sub . g) <$> h i ...(subCong prf.prf (h i))
+    ~~ (prf.sub . g) <$> h i ...(subExtensional prf.prf (h i))
     ~~ prf.sub <$> g <$> h i ...(subAssoc prf.sub g (h i))
   }
 
 export
 lteExtend :
   {p : Property sig k} ->
-  {f : SFin k -> Term sig m} ->
-  {g : SFin k -> Term sig n} ->
+  {f : Fin k -> Term sig m} ->
+  {g : Fin k -> Term sig n} ->
   (prf : f <= g) ->
   p.Prop f ->
   (Extension p g).Prop prf.sub
 lteExtend prf x = p.cong prf.prf x
 
--- Maximal ---------------------------------------------------------------------
+-- Most General ----------------------------------------------------------------
+
+-- public export
+-- record MostGeneral (p : Property sig k) where
 
 public export
 Max : Property sig k -> Property sig k
 Max p = MkProp
-  { Prop = \f => (p.Prop f, forall n. (g : SFin k -> Term sig n) -> p.Prop g -> g <= f)
+  { Prop = \f => (p.Prop f, forall n. (g : Fin 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))
   }
 
@@ -278,8 +281,8 @@ record DClosed (p : Property sig k) where
   constructor MkDClosed
   closed :
     forall m, n.
-    (f : SFin k -> Term sig m) ->
-    (g : SFin k -> Term sig n) ->
+    (f : Fin k -> Term sig m) ->
+    (g : Fin k -> Term sig n) ->
     f <= g ->
     p.Prop g ->
     p.Prop f
@@ -290,18 +293,18 @@ export
 unifiesDClosed : (t, u : Term sig k) -> DClosed (Unifies t u)
 unifiesDClosed t u = MkDClosed (\f, g, prf1, prf2 => Calc $
   |~ f <$> t
-  ~~ (prf1.sub . g) <$> t ...(subCong prf1.prf t)
+  ~~ (prf1.sub . g) <$> t ...(subExtensional prf1.prf t)
   ~~ prf1.sub <$> g <$> t ...(subAssoc prf1.sub g t)
   ~~ prf1.sub <$> g <$> u ...(cong (prf1.sub <$>) prf2)
   ~~ (prf1.sub . g) <$> u ..<(subAssoc prf1.sub g u)
-  ~~ f <$> u              ..<(subCong prf1.prf u))
+  ~~ f <$> u              ..<(subExtensional prf1.prf u))
 
 export
 optimistLemma :
   {ps : Vect _ (Property sig j)} ->
-  {a : SFin j -> Term sig k} ->
-  {f : SFin k -> Term sig m} ->
-  {g : SFin m -> Term sig n} ->
+  {a : Fin j -> Term sig k} ->
+  {f : Fin k -> Term sig m} ->
+  {g : Fin m -> Term sig n} ->
   DClosed p ->
   (Max (Extension p a)).Prop f ->
   (Max (Extension (All ps) (f . a))).Prop g ->
@@ -312,14 +315,14 @@ optimistLemma prf (x, max1) (y, max2) =
     )
   , \h, (x' :: y') =>
     let prf1 = max1 h x' in
-    let y'' = (All ps).cong (\i => trans (subCong prf1.prf (a i)) (subAssoc prf1.sub f (a i))) y' in
+    let y'' = (All ps).cong (\i => trans (subExtensional prf1.prf (a i)) (subAssoc prf1.sub f (a i))) y' in
     let prf2 = max2 prf1.sub y'' in
     MkLte
       { sub = prf2.sub
       , prf = \i => Calc $
         |~ h i
         ~~ prf1.sub <$> f i         ...(prf1.prf i)
-        ~~ (prf2.sub . g) <$> f i   ...(subCong (prf2.prf) (f i))
+        ~~ (prf2.sub . g) <$> f i   ...(subExtensional (prf2.prf) (f i))
         ~~ prf2.sub <$> (g <$> f i) ...(subAssoc prf2.sub g (f i))
       }
   )
@@ -331,8 +334,8 @@ failHead absurd f (x :: xs) = absurd f x
 export
 failTail :
   {ps : Vect _ (Property sig j)} ->
-  {a : SFin j -> Term sig k} ->
-  {f : SFin k -> Term sig m} ->
+  {a : Fin j -> Term sig k} ->
+  {f : Fin k -> Term sig m} ->
   (Max (Extension p a)).Prop f ->
   Nothing (Extension (All ps) (f . a)) ->
   Nothing (Extension (All (p :: ps)) a)
diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index b87ab21..b4f7ebd 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -1,10 +1,6 @@
 module Data.Term.Unify
 
-import Data.DPair
 import Data.Fin.Occurs
-import Data.Fin.Strong
-import Data.Maybe.Properties
-import Data.Singleton
 import Data.Term
 import Data.Term.Property
 import Data.Term.Zipper
@@ -16,10 +12,10 @@ import Syntax.PreorderReasoning
 -- Check -----------------------------------------------------------------------
 
 export
-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 : {k : Nat} -> Fin (S k) -> Term sig (S k) -> Maybe (Term sig k)
+checkAll : {k : Nat} -> Fin (S k) -> Vect n (Term sig (S k)) -> Maybe (Vect n (Term sig 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 []
@@ -27,168 +23,97 @@ checkAll x (t :: ts) = [| check x t :: checkAll x ts |]
 
 -- Properties
 
-export
-checkOccurs :
-  (x : SFin k) ->
-  (zip : Zipper sig k) ->
-  IsNothing (check x (zip + Var' x))
-checkAllOccurs :
-  (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))
-
-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 =
-  appLeftNothingIsNothing
-    (appRightNothingIsNothing (Just (::)) (checkOccurs x zip))
-    (checkAll x ts)
-checkAllOccurs x (FS i) (t :: ts) zip =
-  appRightNothingIsNothing
-    (Just (::) <*> check x t)
-    (checkAllOccurs x i ts zip)
-
-export
-checkNothing :
-  (x : SFin k) ->
-  (t : Term sig k) ->
-  (0 _ : IsNothing (check x t)) ->
-  (zip : Zipper sig k ** t = zip + Var' x)
-checkAllNothing :
-  (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')
-
-checkNothing x (Var 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)
-
-checkAllNothing x t ts prf with (appNothingInverse (Just (::) <*> check x t) (checkAll x ts) prf)
-  _ | Left prf' = case appNothingInverse (Just (::)) (check x t) prf' of
-      Right prf =>
-        let (zip ** prf) = checkNothing x t prf in
-        (FZ ** ts ** zip ** cong (:: ts) prf)
-  checkAllNothing x t (t' :: ts) prf | Right prf' =
-    let (i ** ts ** zip ** prf) = checkAllNothing x t' ts prf' in
-    (FS i ** t :: ts ** zip ** cong (t ::) prf)
-
-export
-checkThin :
-  (x : SFin (S k)) ->
-  (t : Term sig k) ->
-  IsJust (check x (pure (thin x) <$> t))
-checkAllThin :
-  (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 (Op op ts) = mapIsJust (Op op) (checkAllThin x ts)
-
-checkAllThin x [] = ItIsJust
-checkAllThin x (t :: ts) =
-  appIsJust
-    (appIsJust ItIsJust (checkThin x t))
-    (checkAllThin x ts)
+public export
+data CheckProof : Fin (S k) -> Term sig (S k) -> Maybe (Term sig k) -> Type where
+  Occurs : (zip : Zipper sig (S k)) -> res = Nothing -> CheckProof x (zip + Var x) res
+  Stronger : (t : Term sig k) -> res = Just t -> CheckProof x (pure (thin x) <$> t) res
+
+data CheckAllProof : Fin (S k) -> Vect n (Term sig (S k)) -> Maybe (Vect n (Term sig k)) -> Type where
+  OccursAt :
+    (i : Fin (S n)) ->
+    (ts : Vect n (Term sig (S k))) ->
+    (zip : Zipper sig (S k)) ->
+    res = Nothing ->
+    CheckAllProof x (insertAt i (zip + Var x) ts) res
+  AllStronger :
+    (ts : Vect n (Term sig k)) ->
+    res = Just ts ->
+    CheckAllProof x (map (pure (thin x) <$>) ts) res
 
 export
-checkJust :
-  (x : SFin k) ->
-  (t : Term sig k) ->
-  (0 _ : check x t = Just u) ->
-  t = pure (thin x) <$> u
-checkAllJust :
-  (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 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)
-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
-  Calc $
-    |~ Op op ts
-    ~~ pure (thin x) <$> Op op z.fst ...(cong (Op op) prf)
-    ~~ pure (thin x) <$> u           ...(sym $ cong (pure (thin x) <$>) $ snd z.snd)
-
-checkAllJust x [] Refl = Refl
-checkAllJust x (t :: ts) prf =
-  let 0 z = appJustInverse (Just (::) <*> check x t) (checkAll x ts) prf in
-  let 0 w = appJustInverse (Just (::)) (check x t) (fst z.snd.snd) in
-  Calc $
-    |~ t :: ts
-    ~~ map (pure (thin x) <$>) (w.snd.fst :: z.snd.fst)    ...(cong2 (::) (checkJust x t (fst $ snd w.snd.snd)) (checkAllJust x ts (fst $ snd z.snd.snd)))
-    ~~ map (pure (thin x) <$>) (w.fst w.snd.fst z.snd.fst) ...(cong (\f => map (pure (thin x) <$>) (f w.snd.fst z.snd.fst)) $ injective $ fst w.snd.snd)
-    ~~ map (pure (thin x) <$>) (z.fst z.snd.fst)           ...(sym $ cong (\f => map (pure (thin x) <$>) (f z.snd.fst)) $ snd $ snd w.snd.snd)
-    ~~ map (pure (thin x) <$>) us                          ...(sym $ cong (map (pure (thin x) <$>)) $ snd $ snd z.snd.snd)
+checkProof : {k : Nat} -> (x : Fin (S k)) -> (t : Term sig (S k)) -> CheckProof x t (check x t)
+checkAllProof :
+  {k : Nat} ->
+  (x : Fin (S k)) ->
+  (ts : Vect n (Term sig (S k))) ->
+  CheckAllProof x ts (checkAll x ts)
+
+checkProof x (Var y) with (thickProof x y)
+  checkProof x (Var x) | Equal prf = Occurs Top (cong (Var <$>) prf)
+  checkProof x (Var _) | Thinned y prf = Stronger (Var y) (cong (Var <$>) prf)
+checkProof x (Op op ts) with (checkAllProof x ts)
+  checkProof x (Op op _) | OccursAt i ts zip prf = Occurs (Op op i ts zip) (cong (Op op <$>) prf)
+  checkProof x (Op op _) | AllStronger ts prf = Stronger (Op op ts) (cong (Op op <$>) prf)
+
+checkAllProof x [] = AllStronger [] Refl
+checkAllProof x (t :: ts) with (checkProof x t)
+  checkAllProof x (_ :: ts) | Occurs zip prf =
+    OccursAt FZ ts zip (cong (\t => [| t :: checkAll x ts |]) prf)
+  checkAllProof x (_ :: ts) | Stronger u prf with (checkAllProof x ts)
+    checkAllProof x (_ :: _) | Stronger u prf | OccursAt i ts zip prf' =
+      OccursAt (FS i) (_ :: ts) zip (cong2 (\t, ts => [| t :: ts |]) prf prf')
+    checkAllProof x (_ :: _) | Stronger u prf | AllStronger us prf' =
+      AllStronger (u :: us) (cong2 (\t, ts => [| t :: ts |]) prf prf')
 
 -- Single Variable Substitution ------------------------------------------------
 
 export
-for : Term sig (pred k) -> SFin k -> SFin k -> Term sig (pred k)
-(t `for` x) y = maybe t Var' (thick x y)
+for : {k : Nat} -> Term sig k -> Fin (S k) -> Fin (S k) -> Term sig k
+(t `for` x) y = maybe t Var (thick x y)
 
 export
 forRefl :
-  (0 u : Term sig (pred k)) ->
-  (x : SFin k) ->
+  (0 u : Term sig k) ->
+  (x : Fin (S k)) ->
   (u `for` x) x = u
-forRefl u x = cong (maybe u Var') $ extractIsNothing $ thickRefl x
+forRefl u x = cong (maybe u Var) $ thickRefl x
 
 export
 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)
+  (0 t : Term sig k) ->
+  (x : Fin (S k)) ->
+  (t `for` x) . thin x .=. Var
+forThin t x i = cong (maybe t Var) (thickThin x i)
 
 export
 forUnifies :
-  (x : SFin k) ->
+  (x : Fin (S k)) ->
   (t : Term sig k) ->
-  (0 _ : check x t = Just u) ->
-  (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)
-  ~~ u                                   ...(subUnit u)
-  ~~ (u `for` x) <$> Var' x              ...(sym $ forRefl u x)
+  (t `for` x) <$> pure (thin x) <$> t = (t `for` x) <$> Var x
+forUnifies x t = Calc $
+  |~ (t `for` x) <$> pure (thin x) <$> t
+  ~~ (t `for` x) . thin x <$> t          ...(sym $ subAssoc (t `for` x) (pure (thin x)) t)
+  ~~ Var <$> t                           ...(subExtensional (forThin t x) t)
+  ~~ t                                   ...(subUnit t)
+  ~~ (t `for` x) <$> Var x               ...(sym $ forRefl t x)
 
 -- Substitution List -----------------------------------------------------------
 
 public export
 data AList : Signature -> Nat -> Nat -> Type where
   Lin : AList sig n n
-  (:<) : AList sig k n -> (Term sig k, SFin (S k)) -> AList sig (S k) n
+  (:<) : AList sig k n -> (Term sig k, Fin (S k)) -> AList sig (S k) n
 
 %name AList sub
 
 namespace Exists
   public export
-  (:<) : Exists (AList sig n) -> (Term sig n, SFin (S n)) -> Exists (AList sig (S n))
+  (:<) : Exists (AList sig n) -> (Term sig n, Fin (S n)) -> Exists (AList sig (S n))
   Evidence _ sub :< tx = Evidence _ (sub :< tx)
 
 export
-eval : AList sig k n -> SFin k -> Term sig n
-eval [<] = Var'
+eval : {k : Nat} -> AList sig k n -> Fin k -> Term sig n
+eval [<] = Var
 eval (sub :< (t, x)) = eval sub . (t `for` x)
 
 export
@@ -199,11 +124,6 @@ sub ++ sub1 :< tx = (sub ++ sub1) :< tx
 -- Properties
 
 export
-recover : Singleton k -> AList sig k n -> Singleton n
-recover x [<] = x
-recover x (sub :< _) = recover (pure pred <*> x) sub
-
-export
 evalHomo :
   (0 sub2 : AList sig k n) ->
   (sub1 : AList sig j k) ->
@@ -211,7 +131,7 @@ evalHomo :
 evalHomo sub2 [<] i = Refl
 evalHomo sub2 (sub1 :< (t, x)) i = Calc $
   |~ eval (sub2 ++ sub1) <$> (t `for` x) i
-  ~~ (eval sub2 . eval sub1) <$> (t `for` x) i ...(subCong (evalHomo sub2 sub1) ((t `for` x) i))
+  ~~ (eval sub2 . eval sub1) <$> (t `for` x) i ...(subExtensional (evalHomo sub2 sub1) ((t `for` x) i))
   ~~ eval sub2 <$> eval sub1 <$> (t `for` x) i ...(subAssoc (eval sub2) (eval sub1) ((t `for` x) i))
 
 export
@@ -233,180 +153,208 @@ appendAssoc sub3 sub2 (sub1 :< tx) = cong (:< tx) (appendAssoc sub3 sub2 sub1)
 coerce : {0 op, op' : sig.Op} -> op = op' -> Vect op'.fst a -> Vect op.fst a
 coerce Refl = id
 
-flexFlex : SFin (S n) -> SFin (S n) -> Exists (AList sig (S n))
-flexFlex x y = case thick x y of
-  Just z => Evidence _ [<(Var' z, x)]
-  Nothing => Evidence _ [<]
+flexFlex : {n : Nat} -> Fin n -> Fin n -> (k ** AList sig n k)
+flexFlex {n = S n} x y = case thick x y of
+  Just z => (_ **[<(Var z, x)])
+  Nothing => (_ ** [<])
 
-flexRigid : SFin (S n) -> Term sig (S n) -> Maybe (Exists (AList sig (S n)))
-flexRigid x t = case check x t of
+flexRigid : {n : Nat} -> Fin n -> Term sig n -> Maybe (Exists (AList sig n))
+flexRigid {n = S n} x t = case check x t of
   Just u => Just (Evidence _ [<(u, x)])
   Nothing => Nothing
 
 export
 amgu :
   DecOp sig =>
+  {n : Nat} ->
   (t, u : Term sig n) ->
-  Exists (AList sig n) ->
+  AList sig n k ->
   Maybe (Exists (AList sig n))
 amguAll :
   DecOp sig =>
-  (ts, us : Vect k (Term sig n)) ->
-  Exists (AList sig n) ->
+  {n : Nat} ->
+  (ts, us : Vect j (Term sig n)) ->
+  AList sig n k ->
   Maybe (Exists (AList sig n))
 
 amgu (Op op ts) (Op op' us) acc with (decOp (Evidence _ op) (Evidence _ op'))
   amgu (Op op ts) (Op op us) acc | Yes Refl = amguAll ts us acc
   _ | No neq = Nothing
-amgu (Var x) (Var y) (Evidence _ [<]) = Just (flexFlex x y)
-amgu (Var x) (Op op' us) (Evidence _ [<]) = flexRigid x (Op op' us)
-amgu (Op op ts) (Var y) (Evidence _ [<]) = flexRigid y (Op op ts)
-amgu t@(Var _) u@(Var _) (Evidence _ (sub :< (v, z))) =
-  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) (Evidence _ sub)
-amgu t@(Var _) u@(Op _ _) (Evidence _ (sub :< (v, z))) =
-  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) (Evidence _ sub)
-amgu t@(Op _ _) u@(Var _) (Evidence _ (sub :< (v, z))) =
-  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) (Evidence _ sub)
-
-amguAll [] [] acc = Just acc
+amgu (Var x) (Var y) [<] = Just (Evidence _ (flexFlex x y).snd)
+amgu (Var x) (Op op' us) [<] = flexRigid x (Op op' us)
+amgu (Op op ts) (Var y) [<] = flexRigid y (Op op ts)
+amgu t@(Var _) u@(Var _) (sub :< (v, z)) =
+  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) sub
+amgu t@(Var _) u@(Op _ _) (sub :< (v, z)) =
+  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) sub
+amgu t@(Op _ _) u@(Var _) (sub :< (v, z)) =
+  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) sub
+
+amguAll [] [] acc = Just (Evidence _ acc)
 amguAll (t :: ts) (u :: us) acc = do
   acc <- amgu t u acc
-  amguAll ts us acc
+  amguAll ts us acc.snd
 
 export
-mgu : DecOp sig => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
-mgu t u = amgu t u (Evidence _ [<])
+mgu : DecOp sig => {n : Nat} -> (t, u : Term sig n) -> Maybe (Exists (AList sig n))
+mgu t u = amgu t u [<]
 
 -- Properties
 
 export
 trivialUnify :
-  (0 f : SFin n -> Term sig k) ->
+  (0 f : Fin n -> Term sig k) ->
   (t : Term sig n) ->
-  (Max (Extension (Unifies t t) f)).Prop Var'
+  (Max (Extension (Unifies t t) f)).Prop Var
 trivialUnify f t = (Refl , \g, prf => varMax g)
 
 export
 varElim :
-  (x : SFin (S n)) ->
-  (t : Term sig (S n)) ->
-  (0 _ : check x t = Just u) ->
-  (Max (Unifies (Var x) t)).Prop (u `for` x)
-varElim x t prf =
-  ( sym $ forUnifies x t prf
-  , \g, prf' => MkLte (g . thin x) (\i =>
-    case decEq x i of
-      Yes Refl =>
-       Calc $
-        |~ g x
-        ~~ g <$> t                        ...(prf')
-        ~~ g <$> pure (thin x) <$> u      ...(cong (g <$>) $ checkJust i t prf)
-        ~~ (g . thin x) <$> u             ...(sym $ subAssoc g (pure (thin x)) u)
-        ~~ (g . thin x) <$> (u `for` x) x ..<(cong ((g . thin x) <$>) $ forRefl u x)
-      No neq =>
-        let isJust = thickNeq x i neq in
-        let (y ** thickIsJustY) = extractIsJust isJust in
-        let thinXYIsI = thickJust x i thickIsJustY in
-        Calc $
-          |~ g i
-          ~~ g (thin x y)                            ..<(cong g thinXYIsI)
-          ~~ (g . thin x) <$> Var' y                 ...(Refl)
-          ~~ (g . thin x) <$> (u `for` x) (thin x y) ..<(cong ((g . thin x) <$>) $ forThin u x y)
-          ~~ (g . thin x) <$> (u `for` x) i          ...(cong (((g . thin x) <$>) . (u `for` x)) $ thinXYIsI))
+  {n : Nat} ->
+  (x : Fin (S n)) ->
+  (t : Term sig n) ->
+  (Max (Unifies (Var x) (pure (thin x) <$> t))).Prop (t `for` x)
+varElim x t =
+  ( sym $ forUnifies x t
+  , \g, prf' => MkLte (g . thin x) (lteProof g prf')
   )
+  where
+  lteProof :
+    forall k.
+    (g : Fin (S n) -> Term sig k) ->
+    (Unifies (Var x) (pure (thin x) <$> t)).Prop g ->
+    g .=. (g . thin x) . (t `for` x)
+  lteProof g prf i with (thickProof x i)
+    lteProof g prf _ | Equal prf' = Calc $
+      |~ g x
+      ~~ g <$> pure (thin x) <$> t    ...(prf)
+      ~~ g . thin x <$> t             ..<(subAssoc g (pure (thin x)) t)
+      ~~ g . thin x <$> (t `for` x) x ..<(cong ((g . thin x <$>) . maybe t Var) prf')
+    lteProof g prf _ | Thinned i prf' = sym $ cong (g . thin x <$>) (forThin t x i)
 
 flexFlexUnifies :
-  (x, y : SFin (S n)) ->
+  {n : Nat} ->
+  (x, y : Fin n) ->
   (Max {sig} (Unifies (Var x) (Var y))).Prop (eval (flexFlex x y).snd)
-flexFlexUnifies x y with (thick x y) proof prf
-  _ | Just z =
-    (Max (Unifies (Var x) (Var y))).cong
-      (\i => sym $ subUnit ((Var' z `for` x) i))
-      (varElim x (Var y) (cong (map Var') prf))
-  _ | Nothing =
-    rewrite thickNothing x y (rewrite prf in ItIsNothing) in
-    trivialUnify Var' (Var y)
-
-flexRigidUnifies :
-  (x : SFin (S n)) ->
-  (t : Term sig (S n)) ->
-  (0 _ : flexRigid x t = Just sub) ->
-  (Max (Unifies (Var x) t)).Prop (eval sub.snd)
-flexRigidUnifies x t ok with (check x t) proof prf
-  flexRigidUnifies x t Refl | Just u =
-    (Max (Unifies (Var x) t)).cong
-      (\i => sym $ subUnit ((u `for` x) i))
-      (varElim x t prf)
-
-flexRigidFails :
-  (x : SFin (S k)) ->
-  (op : sig.Operator j) ->
-  (ts : Vect j (Term sig (S k))) ->
-  (0 _ : IsNothing (flexRigid x (Op op ts))) ->
-  Nothing (Unifies (Var x) (Op op ts))
-flexRigidFails x op ts isNothing f prf' with (check x (Op op ts)) proof prf
-  _ | Nothing =
-    let
-      (zip ** occurs) = checkNothing x (Op op ts) (rewrite prf in ItIsNothing)
-      cycle : (f x = (f <$> zip) + f x)
-      cycle = Calc $
-        |~ f x
-        ~~ f <$> Op op ts    ...(prf')
-        ~~ f <$> zip + Var x ...(cong (f <$>) occurs)
-        ~~ (f <$> zip) + f x ...(actionHomo f zip (Var x))
-      zipIsTop : (zip = Top)
-      zipIsTop = invertActionTop zip $ noCycles (f <$> zip) (f x) (sym cycle)
-      opIsVar : (Op op ts = Var x)
-      opIsVar = trans occurs (cong (+ Var x) zipIsTop)
-    in
-    absurd opIsVar
+flexFlexUnifies {n = S n} x y with (thickProof x y)
+  flexFlexUnifies {n = S n} x _ | Equal prf =
+    rewrite prf in
+    trivialUnify Var (Var x)
+  flexFlexUnifies {n = S n} x _ | Thinned y prf =
+    rewrite prf in
+    (Max (Unifies (Var x) (Var _))).cong
+      (\i => sym $ subUnit ((Var y `for` x) i))
+      (varElim x (Var y))
+
+data FlexRigidProof : Fin n -> Term sig n -> Maybe (Exists (AList sig n)) -> Type where
+  NoUnifier : Nothing (Unifies (Var x) t) -> res = Nothing -> FlexRigidProof x t res
+  ElimVar :
+    {n : Nat} ->
+    (sub : AList sig k n) ->
+    (mgu : (Max (Unifies (Var x) t)).Prop (eval sub)) ->
+    res = Just (Evidence _ sub) ->
+    FlexRigidProof x t res
+
+flexRigidProof :
+  {n : Nat} ->
+  (x : Fin n) ->
+  (op : sig.Operator k) ->
+  (ts : Vect k (Term sig n)) ->
+  FlexRigidProof x (Op op ts) (flexRigid x (Op op ts))
+flexRigidProof {n = S n} x op ts with (checkProof x (Op op ts))
+  flexRigidProof x op _ | Occurs zip@(Op op i ts zip') prf =
+    rewrite prf in
+    NoUnifier
+      (\f, prf' =>
+        let
+          cycle : (f x = (f <$> zip) + f x)
+          cycle = Calc $
+           |~ f x
+           ~~ f <$> Op op _     ...(prf')
+           ~~ (f <$> zip) + f x ...(actionHomo f zip (Var x))
+
+          zipIsTop : (zip = Top)
+          zipIsTop = invertActionTop zip $ noCycles (f <$> zip) (f x) (sym cycle)
+
+          opIsVar : Op op (insertAt i (zip' + Var x) ts) = Var x
+          opIsVar = cong (+ Var x) zipIsTop
+        in
+        absurd opIsVar)
+      Refl
+  flexRigidProof x op _ | Stronger (Op op us) prf =
+    rewrite prf in
+    ElimVar
+      [<(Op op us, x)]
+      ((Max (Unifies (Var x) (Op op _))).cong
+        (\i => sym $ subUnit ((Op op us `for` x) i))
+        (varElim x (Op op us)))
+      Refl
 
 stepEquiv :
+  {k : Nat} ->
   (t, u : Term sig (S k)) ->
   (sub : AList sig k j) ->
   (v : Term sig k) ->
-  (x : SFin (S k)) ->
+  (x : Fin (S k)) ->
   Extension (Unifies t u) (eval (sub :< (v, x))) <=>
   Extension (Unifies ((v `for` x) <$> t) ((v `for` x) <$> u)) (eval sub)
 stepEquiv t u sub v x = extendUnify t u (v `for` x) (eval sub)
 
 parameters {auto _ : DecOp sig}
   public export
-  data AmguProof : (t, u : Term sig k) -> Exists (AList sig k) -> Type where
-    Success :
-      {0 sub : Exists (AList sig k)} ->
-      (sub' : Exists (AList sig sub.fst)) ->
-      (Max (Extension (Unifies t u) (eval sub.snd))).Prop (eval sub'.snd) ->
-      amgu t u sub = Just (Evidence sub'.fst (sub'.snd ++ sub.snd)) ->
-      AmguProof t u sub
+  data AmguProof :
+    Term sig k ->
+    Term sig k ->
+    AList sig k n ->
+    Maybe (Exists (AList sig k)) ->
+    Type
+    where
     Failure :
-      {0 sub : Exists (AList sig k)} ->
-      Nothing (Extension (Unifies t u) (eval sub.snd)) ->
-      IsNothing (amgu t u sub) ->
-      AmguProof t u sub
+      Nothing (Extension (Unifies t u) (eval sub)) ->
+      res = Nothing ->
+      AmguProof t u sub res
+    Success :
+      {j : Nat} ->
+      {0 sub : AList sig k n} ->
+      (sub' : AList sig n j) ->
+      (Max (Extension (Unifies t u) (eval sub))).Prop (eval sub') ->
+      res = Just (Evidence _ (sub' ++ sub)) ->
+      AmguProof t u sub res
 
   public export
-  data AmguAllProof : (ts, us : Vect n (Term sig k)) -> Exists (AList sig k) -> Type where
-    SuccessAll :
-      {0 sub : Exists (AList sig k)} ->
-      (sub' : Exists (AList sig sub.fst)) ->
-      (Max (Extension (UnifiesAll ts us) (eval sub.snd))).Prop (eval sub'.snd) ->
-      amguAll ts us sub = Just (Evidence sub'.fst (sub'.snd ++ sub.snd)) ->
-      AmguAllProof ts us sub
+  data AmguAllProof :
+    Vect j (Term sig k) ->
+    Vect j (Term sig k) ->
+    AList sig k n ->
+    Maybe (Exists (AList sig k)) ->
+    Type
+    where
     FailureAll :
-      {0 sub : Exists (AList sig k)} ->
-      Nothing (Extension (UnifiesAll ts us) (eval sub.snd)) ->
-      IsNothing (amguAll ts us sub) ->
-      AmguAllProof ts us sub
+      Nothing (Extension (UnifiesAll ts us) (eval sub)) ->
+      res = Nothing ->
+      AmguAllProof ts us sub res
+    SuccessAll :
+      {j : Nat} ->
+      {0 sub : AList sig k n} ->
+      (sub' : AList sig n j) ->
+      (Max (Extension (UnifiesAll ts us) (eval sub))).Prop (eval sub') ->
+      res = Just (Evidence _ (sub' ++ sub)) ->
+      AmguAllProof ts us sub res
 
 export
-amguProof : DecOp sig => (t, u : Term sig n) -> (sub : Exists (AList sig n)) -> AmguProof t u sub
+amguProof :
+  DecOp sig =>
+  {k, n : Nat} ->
+  (t, u : Term sig k) ->
+  (sub : AList sig k n) ->
+  AmguProof t u sub (amgu t u sub)
 export
 amguAllProof :
   DecOp sig =>
-  (ts, us : Vect k (Term sig n)) ->
-  (sub : Exists (AList sig n)) ->
-  AmguAllProof ts us sub
+  {k, n : Nat} ->
+  (ts, us : Vect j (Term sig k)) ->
+  (sub : AList sig k n) ->
+  AmguAllProof ts us sub (amguAll ts us sub)
 
 amguProof (Op op ts) (Op op' us) sub with (decOp (Evidence _ op) (Evidence _ op')) proof prf
   amguProof (Op op ts) (Op op us) sub | Yes Refl
@@ -414,53 +362,48 @@ amguProof (Op op ts) (Op op' us) sub with (decOp (Evidence _ op) (Evidence _ op'
     _ | SuccessAll sub' val prf' =
       let
         cong :
-          Max (Extension (Unifies (Op op ts) (Op op us)) (eval sub.snd)) <=>
-          Max (Extension (UnifiesAll ts us) (eval sub.snd))
-        cong = maxCong $ extendCong (eval sub.snd) $ unifiesOp op ts us
+          Max (Extension (Unifies (Op op ts) (Op op us)) (eval sub)) <=>
+          Max (Extension (UnifiesAll ts us) (eval sub))
+        cong = maxCong $ extendCong (eval sub) $ unifiesOp op ts us
       in
       Success sub'
-        (cong.rightToLeft (eval sub'.snd) val)
-        (rewrite prf in prf')
+        (cong.rightToLeft (eval sub') val)
+        prf'
     _ | FailureAll absurd prf' =
       Failure
-        (nothingEquiv (symmetric $ extendCong (eval sub.snd) $ unifiesOp op ts us) absurd)
-        (rewrite prf in prf')
+        (nothingEquiv (symmetric $ extendCong (eval sub) $ unifiesOp op ts us) absurd)
+        prf'
   _ | No neq =
     Failure
       (\f, prf => neq $ opInjectiveOp prf)
-      (rewrite prf in ItIsNothing)
-amguProof (Var x) (Var y) (Evidence _ [<]) with (thick x y) proof prf
-  _ | Just z = Success (flexFlex x y) (flexFlexUnifies x y) (rewrite prf in Refl)
-  _ | Nothing = Success (flexFlex x y) (flexFlexUnifies x y) (rewrite prf in Refl)
-amguProof (Var x) (Op op' us) (Evidence _ [<]) with (flexRigid x (Op op' us)) proof prf
-  _ | Just sub@(Evidence _ _) = Success sub (flexRigidUnifies x (Op op' us) prf) prf
-  _ | Nothing =
-    Failure
-      (flexRigidFails x op' us (rewrite prf in ItIsNothing))
-      (rewrite prf in ItIsNothing)
-amguProof (Op op ts) (Var y) (Evidence _ [<]) with (flexRigid y (Op op ts)) proof prf
-  _ | Just sub@(Evidence _ sub') =
+      Refl
+amguProof (Var x) (Var y) [<] =
+  Success
+    (flexFlex x y).snd
+    (flexFlexUnifies x y)
+    Refl
+amguProof (Var x) (Op op' us) [<] with (flexRigidProof x op' us)
+  _ | NoUnifier absurd prf = Failure absurd prf
+  _ | ElimVar sub val prf = Success sub val prf
+amguProof (Op op ts) (Var y) [<] with (flexRigidProof y op ts)
+  _ | NoUnifier absurd prf =
     let
       cong :
-        Max (Extension (Unifies (Var y) (Op op ts)) Var') <=>
-        Max (Extension (Unifies (Op op ts) (Var y)) Var')
-      cong = maxCong $ extendCong Var' $ unifiesSym (Var y) (Op op ts)
+        Nothing (Extension (Unifies (Var y) (Op op ts)) Var) ->
+        Nothing (Extension (Unifies (Op op ts) (Var y)) Var)
+      cong = nothingEquiv $ extendCong Var $ unifiesSym (Var y) (Op op ts)
     in
-    Success sub
-      (cong.leftToRight (eval sub.snd) (flexRigidUnifies y (Op op ts) prf))
-      prf
-  _ | Nothing =
+    Failure (cong absurd) prf
+  _ | ElimVar sub val prf =
     let
       cong :
-        Nothing (Extension (Unifies (Var y) (Op op ts)) Var') ->
-        Nothing (Extension (Unifies (Op op ts) (Var y)) Var')
-      cong = nothingEquiv $ extendCong Var' $ unifiesSym (Var y) (Op op ts)
+        Max (Extension (Unifies (Var y) (Op op ts)) Var) <=>
+        Max (Extension (Unifies (Op op ts) (Var y)) Var)
+      cong = maxCong $ extendCong Var $ unifiesSym (Var y) (Op op ts)
     in
-    Failure
-      (cong $ flexRigidFails y op ts (rewrite prf in ItIsNothing))
-      (rewrite prf in ItIsNothing)
-amguProof (Var x) (Var y) (Evidence l (sub :< (v, z)))
-  with (amguProof ((v `for` z) x) ((v `for` z) y) (Evidence _ sub))
+    Success sub (cong.leftToRight _ val) prf
+amguProof (Var x) (Var y) (sub :< (v, z))
+  with (amguProof ((v `for` z) x) ((v `for` z) y) sub)
   _ | Success sub' val prf =
     let
       cong' :
@@ -469,14 +412,14 @@ amguProof (Var x) (Var y) (Evidence l (sub :< (v, z)))
       cong' = maxCong $ stepEquiv (Var x) (Var y) sub v z
     in
     Success sub'
-      (cong'.rightToLeft (eval sub'.snd) val)
+      (cong'.rightToLeft (eval sub') val)
       (cong (map (:< (v, z))) prf)
   _ | Failure absurd prf =
     Failure
       (nothingEquiv (symmetric $ stepEquiv (Var x) (Var y) sub v z) absurd)
-      (mapNothing (:< (v, z)) prf)
-amguProof (Var x) (Op op' us) (Evidence _ (sub :< (v, z)))
-  with (amguProof ((v `for` z) x) ((v `for` z) <$> Op op' us) (Evidence _ sub))
+      (rewrite prf in Refl)
+amguProof (Var x) (Op op' us) (sub :< (v, z))
+  with (amguProof ((v `for` z) x) ((v `for` z) <$> Op op' us) sub)
   _ | Success sub' val prf =
     let
       cong' :
@@ -485,14 +428,14 @@ amguProof (Var x) (Op op' us) (Evidence _ (sub :< (v, z)))
       cong' = maxCong $ stepEquiv (Var x) (Op op' us) sub v z
     in
     Success sub'
-      (cong'.rightToLeft (eval sub'.snd) val)
+      (cong'.rightToLeft (eval sub') val)
       (cong (map (:< (v, z))) prf)
   _ | Failure absurd prf =
     Failure
       (nothingEquiv (symmetric $ stepEquiv (Var x) (Op op' us) sub v z) absurd)
-      (mapNothing (:< (v, z)) prf)
-amguProof (Op op ts) (Var y) (Evidence _ (sub :< (v, z)))
-  with (amguProof ((v `for` z) <$> Op op ts) ((v `for` z) y) (Evidence _ sub))
+      (rewrite prf in Refl)
+amguProof (Op op ts) (Var y) (sub :< (v, z))
+  with (amguProof ((v `for` z) <$> Op op ts) ((v `for` z) y) sub)
   _ | Success sub' val prf =
     let
       cong' :
@@ -501,38 +444,38 @@ amguProof (Op op ts) (Var y) (Evidence _ (sub :< (v, z)))
       cong' = maxCong $ stepEquiv (Op op ts) (Var y) sub v z
     in
     Success sub'
-      (cong'.rightToLeft (eval sub'.snd) val)
+      (cong'.rightToLeft (eval sub') val)
       (cong (map (:< (v, z))) prf)
   _ | Failure absurd prf =
     Failure
       (nothingEquiv (symmetric $ stepEquiv (Op op ts) (Var y) sub v z) absurd)
-      (mapNothing (:< (v, z)) prf)
+      (rewrite prf in Refl)
 
-amguAllProof [] [] (Evidence _ sub) =
-  SuccessAll (Evidence _ [<])
+amguAllProof [] [] sub =
+  SuccessAll [<]
     ([], \g, x => varMax g)
     (sym $ cong (\sub => Just (Evidence _ sub)) $ appendUnitLeft sub)
 amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
-  _ | Success sub' val prf with (amguAllProof ts us (Evidence _ (sub'.snd ++ sub.snd)))
+  _ | Success sub' val prf with (amguAllProof ts us (sub' ++ sub))
     _ | SuccessAll sub'' val' prf' =
       let
         cong' =
           maxCong $
-          extendCong2 (evalHomo sub'.snd sub.snd) (reflexive {x = UnifiesAll ts us})
+          extendCong2 (evalHomo sub' sub) (reflexive {x = UnifiesAll ts us})
         opt =
           optimistLemma (unifiesDClosed t u) val $
-          cong'.leftToRight (eval sub''.snd) val'
+          cong'.leftToRight (eval sub'') val'
       in
-      SuccessAll (Evidence _ (sub''.snd ++ sub'.snd))
-        ((Max (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub.snd))).cong
-          (\i => sym $ evalHomo sub''.snd sub'.snd i)
+      SuccessAll (sub'' ++ sub')
+        ((Max (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub))).cong
+          (\i => sym $ evalHomo sub'' sub' i)
           opt)
         (rewrite prf in rewrite prf' in
-          cong (\sub => Just (Evidence sub''.fst sub)) $
-          appendAssoc sub''.snd sub'.snd sub.snd)
+          cong (\sub => Just (Evidence _ sub)) $
+          appendAssoc sub'' sub' sub)
     _ | FailureAll absurd prf' =
       let
-        cong' = extendCong2 (evalHomo sub'.snd sub.snd) (reflexive {x = UnifiesAll ts us})
+        cong' = extendCong2 (evalHomo sub' sub) (reflexive {x = UnifiesAll ts us})
       in
       FailureAll
         (failTail val $ nothingEquiv cong' absurd)
@@ -540,24 +483,24 @@ amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
   _ | Failure absurd prf =
     FailureAll
       (failHead absurd)
-      (bindNothing prf (amguAll ts us))
+      (rewrite prf in Refl)
 
 parameters {auto _ : DecOp sig}
   namespace MguProof
     public export
-    data MguProof : (t, u : Term sig k) -> Type where
+    data MguProof : (t, u : Term sig k) -> Maybe (Exists (AList sig k)) -> Type where
       Success :
-        (sub : Exists (AList sig k)) ->
-        (Max (Unifies t u)).Prop (eval sub.snd) ->
-        mgu t u = Just sub ->
-        MguProof t u
+        (sub : AList sig k n) ->
+        (Max (Unifies t u)).Prop (eval sub) ->
+        res = Just (Evidence _ sub) ->
+        MguProof t u res
       Failure :
         Nothing (Unifies t u) ->
-        IsNothing (mgu t u) ->
-        MguProof t u
+        res = Nothing ->
+        MguProof t u res
 
 export
-mguProof : DecOp sig => (t, u : Term sig k) -> MguProof t u
-mguProof t u with (amguProof t u (Evidence _ [<]))
-  _ | Success (Evidence _ sub) val prf = Success (Evidence _ sub) val prf
+mguProof : DecOp sig => {k : Nat} -> (t, u : Term sig k) -> MguProof t u (mgu t u)
+mguProof t u with (amguProof t u [<])
+  _ | Success sub val prf = Success sub val prf
   _ | Failure absurd prf = Failure absurd prf
diff --git a/src/Data/Term/Zipper.idr b/src/Data/Term/Zipper.idr
index ddc0797..05cdfc9 100644
--- a/src/Data/Term/Zipper.idr
+++ b/src/Data/Term/Zipper.idr
@@ -2,44 +2,33 @@ module Data.Term.Zipper
 
 import Data.DPair
 import Data.Fin.Occurs
-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) ->
+  (i : Fin (S k)) ->
   (x : a) ->
-  (xs : Vect (pred k) a) ->
-  map f (insertAt' i x xs) = insertAt' i (f x) (map f xs)
+  (xs : Vect 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
+  (i : Fin (S k)) ->
+  (xs : Vect (S k) a) ->
+  insertAt i (index i xs) (deleteAt i xs) = xs
 insertAtDeleteAt FZ (x :: xs) = Refl
-insertAtDeleteAt (FS i) (x :: xs) = cong (x ::) $ insertAtDeleteAt i xs
+insertAtDeleteAt (FS i) (x :: xs@(_ :: _)) = cong (x ::) $ insertAtDeleteAt i xs
 
 indexInsertAt :
-  (i : SFin k) ->
+  (i : Fin (S k)) ->
   (x : a) ->
-  (xs : Vect (pred k) a) ->
-  index (strongToFin i) (insertAt' i x xs) = x
+  (xs : Vect k a) ->
+  index i (insertAt i x xs) = x
 indexInsertAt FZ x xs = Refl
 indexInsertAt (FS i) x (y :: xs) = indexInsertAt i x xs
 
@@ -48,7 +37,7 @@ indexInsertAt (FS i) x (y :: xs) = indexInsertAt i x xs
 public export
 data Zipper : Signature -> Nat -> Type where
   Top : Zipper sig n
-  Op : sig.Operator k -> SFin k -> Vect (pred k) (Term sig n) -> Zipper sig n -> Zipper sig n
+  Op : sig.Operator (S k) -> Fin (S k) -> Vect k (Term sig n) -> Zipper sig n -> Zipper sig n
 
 %name Zipper zip
 
@@ -81,7 +70,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
 
@@ -92,12 +81,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
-(<$>) : (SFin k -> Term sig n) -> Zipper sig k -> Zipper sig n
+(<$>) : (Fin 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)
 
@@ -105,15 +94,15 @@ f <$> Op op i ts zip = Op op i (map (f <$>) ts) (f <$> zip)
 
 export
 actionHomo :
-  (0 f : SFin k -> Term sig n) ->
+  (0 f : Fin 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)
 
 export
 invertActionTop : (zip : Zipper sig k) -> (0 _ : f <$> zip = Top) -> zip = Top
@@ -121,14 +110,14 @@ invertActionTop Top prf = Refl
 
 -- Cycles ----------------------------------------------------------------------
 
-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
+pivotAt : sig.Operator (S k) -> Fin (S k) -> Vect (S k) (Term sig n) -> Zipper sig n
+pivotAt op i ts = Op op i (deleteAt i ts) Top
 
 actionPivotAt :
-  (op : sig.Operator k) ->
-  (i : SFin k) ->
-  (ts : Vect k (Term sig n)) ->
-  pivotAt op i ts + index (strongToFin i) ts = Op op ts
+  (op : sig.Operator (S k)) ->
+  (i : Fin (S k)) ->
+  (ts : Vect (S k) (Term sig n)) ->
+  pivotAt op i ts + index 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)
@@ -137,26 +126,23 @@ pivotNotTop (Op op' j us zip) prf impossible
 export
 noCycles : (zip : Zipper sig k) -> (t : Term sig k) -> zip + t = t -> zip = Top
 noCycles Top t prf = Refl
-noCycles (Op {k} op i ts zip') t@(Op {k = j} op' us) prf =
+noCycles (Op {k} op i ts zip') t@(Op {k = S j} op' us@(_ :: _)) prf =
   void $ pivotNotTop zip' prf''
   where
-  i' : Fin k
-  i' = strongToFin i
-
-  I : SFin j
-  I = replace {p = SFin} (opInjectiveLen prf) i
+  i' : Fin (S k)
+  i' = i
 
-  I' : Fin j
-  I' = strongToFin I
+  I : Fin (S j)
+  I = replace {p = Fin} (opInjectiveLen prf) 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'