Add compilation to scheme.

Extract parser as an independent project.

28 files changed, 1010 insertions, 2077 deletions

diff --git a/src/Inky.idr b/src/Inky.idr
index 649c620..66124c6 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -6,11 +6,13 @@ import Control.App
 import Control.App.Console
 import Control.App.FileIO
 
-import Inky.Decidable
-import Inky.Decidable.Maybe
-import Inky.Parser
+import Flap.Decidable
+import Flap.Decidable.Maybe
+import Flap.Parser
+
 import Inky.Term
 import Inky.Term.Checks
+import Inky.Term.Compile
 import Inky.Term.Desugar
 import Inky.Term.Parser
 import Inky.Term.Pretty
@@ -29,6 +31,10 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 %hide Collie.Modifiers.infix.(::=)
 
+record Erased (a : Type) where
+  constructor Forget
+  0 value : a
+
 -- Actions ---------------------------------------------------------------------
 
 lexInkyString : HasErr String es => String -> App es (List (WithBounds InkyToken))
@@ -55,17 +61,20 @@ parseTerm toks = do
     | Left msg => throw msg
   pure t
 
-checkType : HasErr String es => Ty [<] -> App es ()
+checkType : HasErr String es => (a : Ty [<]) -> App es (Erased $ WellFormed a)
 checkType a = do
   let True `Because` wf = wellFormed a
     | False `Because` bad => throw "type ill-formed"
-  pure ()
+  pure (Forget wf)
 
-checkTerm : (a : Ty [<]) -> (t : Term mode m [<] [<]) -> HasErr (NotChecks [<] [<] a t) es => App es ()
+checkTerm :
+  (a : Ty [<]) -> (t : Term mode m [<] [<]) ->
+  HasErr (NotChecks [<] [<] a t) es =>
+  App es (Erased $ Checks [<] [<] a t)
 checkTerm a t = do
   let True `Because` prf = checks [<] [<] a t
     | False `Because` contra => throw contra
-  pure ()
+  pure (Forget prf)
 
 printType :
   PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
@@ -89,6 +98,18 @@ printCheckError contra =
   map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $
   prettyNotChecks contra
 
+compileTerm :
+  PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
+  {a : Ty [<]} ->
+  {t : Term mode m [<] [<]} ->
+  (0 wf : WellFormed a) ->
+  (0 prf : Checks [<] [<] a t) ->
+  App es ()
+compileTerm wf prf =
+  primIO $ renderIO $ layoutSmart opts $
+  pretty "(use-modules (ice-9 match))" <+> line <+>
+  parens (hang 1 $ pretty "define main" <+> line <+> group (compileChecks [<] [<] wf prf))
+
 readFile : FileIO es => File -> App es String
 readFile f = do
   content <- read [<] f
@@ -147,6 +168,21 @@ Inky = MkCommand
       , modifiers = []
       , arguments = none
       }
+    , "compile" ::= MkCommand
+      { description = """
+        compile to scheme
+        """
+      , subcommands =
+        [ "term" ::= MkCommand
+          { description = "compile a term"
+          , subcommands = []
+          , modifiers = ["--type" ::= option "type to check against" filePath]
+          , arguments = filePath
+          }
+        ]
+      , modifiers = []
+      , arguments = none
+      }
     ]
   , modifiers = []
   , arguments = none
@@ -212,7 +248,7 @@ main = run {l = MayThrow} $ do
           txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
           toks <- handle {err = String} (lexInkyString txt) pure abortErr
           a <- handle {err = String} (parseType toks) pure abortErr
-          handle {err = String} (checkType a) pure abortErr
+          handle {err = String} (checkType a) (const $ pure ()) abortErr
         ]
       , "term" ::=
         [ \cmd => do
@@ -227,11 +263,36 @@ main = run {l = MayThrow} $ do
                 txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
                 toks <- handle {err = String} (lexInkyString txt) pure abortErr
                 a <- handle {err = String} (parseType toks) pure abortErr
-                handle {err = String} (checkType a) pure abortErr
+                handle {err = String} (checkType a) (const $ pure ()) abortErr
                 pure a)
               type
-          handle {err = NotChecks [<] [<] a t} (checkTerm a t) pure
+          handle {err = NotChecks [<] [<] a t} (checkTerm a t) (const $ pure ())
             (\contra => do printCheckError contra; primIO exitFailure)
         ]
       ]
+    , "compile" ::=
+      [ const showHelp
+      , "term" ::=
+        [ \cmd => do
+          let path = cmd.arguments
+          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
+          toks <- handle {err = String} (lexInkyString txt) pure abortErr
+          t <- handle {err = String} (parseTerm toks) pure abortErr
+          let [type] = cmd.modifiers.content
+          Element a wf <-
+            the (App _ (Subset (Ty [<]) WellFormed)) $
+            maybe (pure (Element (TArrow TNat TNat) %search))
+              (\path => do
+                txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
+                toks <- handle {err = String} (lexInkyString txt) pure abortErr
+                a <- handle {err = String} (parseType toks) pure abortErr
+                Forget wf <- handle {err = String} (checkType a) pure abortErr
+                pure (Element a wf))
+              type
+          Forget prf <-
+            handle {err = NotChecks [<] [<] a t} (checkTerm a t) pure
+              (\contra => do printCheckError contra; primIO exitFailure)
+          compileTerm wf prf
+        ]
+      ]
     ]
diff --git a/src/Inky/Data/Assoc.idr b/src/Inky/Data/Assoc.idr
deleted file mode 100644
index 0818ba3..0000000
--- a/src/Inky/Data/Assoc.idr
+++ /dev/null
@@ -1,38 +0,0 @@
-module Inky.Data.Assoc
-
-export
-infix 2 :-
-
-public export
-record Assoc (a : Type) where
-  constructor (:-)
-  name : String
-  value : a
-
-public export
-Functor Assoc where
-  map f x = x.name :- f x.value
-
-namespace Irrelevant
-  public export
-  record Assoc0 (0 a : Type) (n : String) where
-    constructor (:-)
-    0 name : String
-    {auto 0 prf : n = name}
-    value : a
-
-  public export
-  map : (a -> b) -> Assoc0 a n -> Assoc0 b n
-  map f (n :- x) = n :- f x
-
-namespace Contexts
-  public export
-  record Assoc0 (0 p : a -> Type) (x : Assoc a) where
-    constructor (:-)
-    0 name : String
-    {auto 0 prf : x.name = name}
-    value : p x.value
-
-  public export
-  map : (forall x. p x -> q x) -> forall x. Assoc0 p x -> Assoc0 q x
-  map f (n :- px) = n :- f px
diff --git a/src/Inky/Data/Context.idr b/src/Inky/Data/Context.idr
deleted file mode 100644
index 4c5f6cf..0000000
--- a/src/Inky/Data/Context.idr
+++ /dev/null
@@ -1,34 +0,0 @@
-module Inky.Data.Context
-
-import public Inky.Data.Assoc
-import public Inky.Data.SnocList
-
-import Inky.Data.SnocList.Quantifiers
-
--- Contexts --------------------------------------------------------------------
-
-public export
-Context : Type -> Type
-Context a = SnocList (Assoc a)
-
-public export
-(.names) : Context a -> SnocList String
-[<].names = [<]
-(ctx :< nx).names = ctx.names :< nx.name
-
-export
-mapNames : (0 f : a -> b) -> (ctx : Context a) -> (map (map f) ctx).names = ctx.names
-mapNames f [<] = Refl
-mapNames f (ctx :< nx) = cong (:< nx.name) $ mapNames f ctx
-
--- Construction ----------------------------------------------------------------
-
-public export
-fromAll : {sx : SnocList String} -> All (Assoc0 a) sx -> Context a
-fromAll [<] = [<]
-fromAll {sx = sx :< n} (ctx :< (_ :- x)) = fromAll ctx :< (n :- x)
-
-export
-fromAllNames : {sx : SnocList String} -> (ctx : All (Assoc0 a) sx) -> (fromAll ctx).names = sx
-fromAllNames [<] = Refl
-fromAllNames {sx = sx :< n} (ctx :< (k :- x)) = cong (:< n) $ fromAllNames ctx
diff --git a/src/Inky/Data/Context/Var.idr b/src/Inky/Data/Context/Var.idr
deleted file mode 100644
index 4741580..0000000
--- a/src/Inky/Data/Context/Var.idr
+++ /dev/null
@@ -1,117 +0,0 @@
-module Inky.Data.Context.Var
-
-import Data.DPair
-import Data.Singleton
-import Inky.Data.Context
-import Inky.Data.SnocList.Elem
-import Inky.Decidable
-import Inky.Decidable.Maybe
-
-export
-prefix 2 %%, %%%
-
-public export
-record Var (ctx : Context a) (x : a) where
-  constructor (%%)
-  0 name : String
-  {auto pos : Elem (name :- x) ctx}
-
-%name Var i, j, k
-
-public export
-toVar : Elem (n :- x) ctx -> Var ctx x
-toVar pos = (%%) n {pos}
-
-public export
-ThereVar : Var ctx x -> Var (ctx :< ny) x
-ThereVar i = toVar (There i.pos)
-
-export
-Show (Var ctx x) where
-  show i = show (elemToNat i.pos)
-
--- Basic Properties ---------------------------------------------------------
-
-export
-toVarCong :
-  {0 n, k : String} -> {0 x, y : a} ->
-  {0 i : Elem (n :- x) ctx} -> {0 j : Elem (k :- y) ctx} ->
-  i ~=~ j -> toVar i ~=~ toVar j
-toVarCong Refl = Refl
-
-export
-posCong : {0 i : Var ctx x} -> {0 j : Var ctx y} -> i = j -> i.pos ~=~ j.pos
-posCong Refl = Refl
-
-export
-toVarInjective :
-  {0 n, k : String} -> {0 x, y : a} ->
-  {i : Elem (n :- x) ctx} -> {j : Elem (k :- y) ctx} ->
-  (0 _ : toVar i ~=~ toVar j) -> i ~=~ j
-toVarInjective prf = toNatInjective $ toNatCong $ posCong prf
-
-export
-posInjective : {i : Var ctx x} -> {j : Var ctx y} -> (0 _ : i.pos ~=~ j.pos) -> i ~=~ j
-posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf
-
--- Decidable Equality ----------------------------------------------------------
-
-public export
-decEq : (i : Var ctx x) -> (j : Var ctx y) -> Dec' (i ~=~ j)
-decEq i j =
-  mapDec (\prf => irrelevantEq $ posInjective prf) posCong $
-  decEq i.pos j.pos
-
--- Weakening -------------------------------------------------------------------
-
-public export
-wknL : (len : LengthOf ctx2) => Var ctx1 x -> Var (ctx1 ++ ctx2) x
-wknL i = toVar $ wknL i.pos len
-
-public export
-wknR : Var ctx1 x -> Var (ctx2 ++ ctx1) x
-wknR i = toVar $ wknR i.pos
-
-public export
-split : {auto len : LengthOf ctx2} -> Var (ctx1 ++ ctx2) x -> Either (Var ctx1 x) (Var ctx2 x)
-split i = bimap toVar toVar $ split len i.pos
-
-public export
-lift :
-  {auto len : LengthOf ctx3} ->
-  (forall x. Var ctx1 x -> Var ctx2 x) ->
-  Var (ctx1 ++ ctx3) x -> Var (ctx2 ++ ctx3) x
-lift f = either (wknL {len} . f) wknR . split {len}
-
--- Names -----------------------------------------------------------------------
-
-export
-nameOf : {ctx : Context a} -> (i : Var ctx x) -> Singleton i.name
-nameOf i = [| (nameOf i.pos).name |]
-
--- Search ----------------------------------------------------------------------
-
-export
-lookup : (n : String) -> (ctx : Context a) -> Maybe (x ** Var ctx x)
-lookup n ctx =
-  case decLookup n ctx of
-    Just x `Because` pos => Just (x ** toVar pos)
-    Nothing `Because` _ => Nothing
-
-namespace Search
-  public export
-  data VarPos : String -> a -> (ctx : Context a) -> Type where
-    [search ctx]
-    Here : VarPos n x (ctx :< (n :- x))
-    There : VarPos n x ctx -> VarPos n x (ctx :< ky)
-
-  %name VarPos pos
-
-  public export
-  toElem : VarPos n x ctx -> Elem (n :- x) ctx
-  toElem Here = Here
-  toElem (There pos) = There (toElem pos)
-
-  public export
-  (%%%) : (0 n : String) -> {auto pos : VarPos n x ctx} -> Var ctx x
-  (%%%) n {pos} = toVar $ toElem pos
diff --git a/src/Inky/Data/Fun.idr b/src/Inky/Data/Fun.idr
index d9acb7d..390745a 100644
--- a/src/Inky/Data/Fun.idr
+++ b/src/Inky/Data/Fun.idr
@@ -1,7 +1,7 @@
 module Inky.Data.Fun
 
-import public Inky.Data.SnocList.Quantifiers
-import Inky.Data.SnocList
+import public Flap.Data.SnocList.Quantifiers
+import Flap.Data.SnocList
 
 public export
 Fun : SnocList Type -> Type -> Type
diff --git a/src/Inky/Data/List.idr b/src/Inky/Data/List.idr
deleted file mode 100644
index 24cb9c0..0000000
--- a/src/Inky/Data/List.idr
+++ /dev/null
@@ -1,13 +0,0 @@
-module Inky.Data.List
-
-public export
-data LengthOf : List a -> Type where
-  Z : LengthOf []
-  S : LengthOf xs -> LengthOf (x :: xs)
-
-%name LengthOf len
-
-public export
-lengthOf : (xs : List a) -> LengthOf xs
-lengthOf [] = Z
-lengthOf (x :: xs) = S (lengthOf xs)
diff --git a/src/Inky/Data/Row.idr b/src/Inky/Data/Row.idr
index 42f18da..8362770 100644
--- a/src/Inky/Data/Row.idr
+++ b/src/Inky/Data/Row.idr
@@ -1,11 +1,12 @@
 module Inky.Data.Row
 
 import public Data.So
-import public Inky.Data.Context
-import public Inky.Data.SnocList.Quantifiers
+import public Flap.Data.Context
+import public Flap.Data.SnocList.Quantifiers
 
-import Inky.Data.SnocList.Elem
-import Inky.Decidable
+import Data.Singleton
+import Flap.Data.SnocList.Elem
+import Flap.Decidable
 
 public export
 FreshIn : String -> SnocList String -> Type
@@ -154,6 +155,33 @@ lookupUnique :
   the (x ** Elem (n :- x) row.context) (x ** i) = (y ** j)
 lookupUnique row i j = doLookupUnique row.context row.fresh i j
 
+notHere :
+  {0 ctx : Context a} ->
+  (i : Elem (n :- x) (ctx :< (l :- y))) ->
+  Not (n = l) -> (j : Elem (n :- x) ctx ** i = There j)
+notHere Here neq = void $ neq Refl
+notHere (There i) _ = (i ** Refl)
+
+doLookupRecompute :
+  (ctx : Context a) -> (0 fresh : AllFresh ctx.names) ->
+  {n : String} -> (0 i : Elem (n :- x) ctx) -> Singleton i
+doLookupRecompute [<] [<] i = void $ absurd i
+doLookupRecompute (ctx :< (l :- x)) (fresh :< freshIn) i with (decEq n l)
+  doLookupRecompute (ctx :< (l :- x)) (fresh :< freshIn) i | True `Because` Refl =
+    replace {p = \x => Singleton x.snd}
+      (doLookupUnique (ctx :< (l :- x)) (fresh :< freshIn) Here i)
+      (Val Here)
+  _ | False `Because` contra =
+    let 0 jeq = notHere i contra in
+    rewrite snd jeq in
+    [| There $ doLookupRecompute ctx fresh (fst jeq) |]
+
+export
+lookupRecompute :
+  (row : Row a) -> {n : String} ->
+  (0 i : Elem (n :- x) row.context) -> Singleton i
+lookupRecompute row i = doLookupRecompute row.context row.fresh i
+
 -- Removal ---------------------------------------------------------------------
 
 dropElemFreshIn :
diff --git a/src/Inky/Data/SnocList.idr b/src/Inky/Data/SnocList.idr
deleted file mode 100644
index 494e8cc..0000000
--- a/src/Inky/Data/SnocList.idr
+++ /dev/null
@@ -1,43 +0,0 @@
-module Inky.Data.SnocList
-
-import public Data.SnocList
-import public Data.SnocList.Operations
-
-import Inky.Decidable.Maybe
-
-public export
-data LengthOf : SnocList a -> Type where
-  Z : LengthOf [<]
-  S : LengthOf sx -> LengthOf (sx :< x)
-
-%name LengthOf len
-
-public export
-lengthOfAppend : LengthOf sx -> LengthOf sy -> LengthOf (sx ++ sy)
-lengthOfAppend len1 Z = len1
-lengthOfAppend len1 (S len2) = S (lengthOfAppend len1 len2)
-
-public export
-lengthOf : (sx : SnocList a) -> LengthOf sx
-lengthOf [<] = Z
-lengthOf (sx :< x) = S (lengthOf sx)
-
-export
-lengthUnique : (len1, len2 : LengthOf sx) -> len1 = len2
-lengthUnique Z Z = Refl
-lengthUnique (S len1) (S len2) = cong S $ lengthUnique len1 len2
-
-export
-isSnoc : (sx : SnocList a) -> Proof (SnocList a, a) (\syy => sx = fst syy :< snd syy) (sx = [<])
-isSnoc [<] = Nothing `Because` Refl
-isSnoc (sx :< x) = Just (sx, x) `Because` Refl
-
-public export
-replicate : Nat -> a -> SnocList a
-replicate 0 x = [<]
-replicate (S n) x = replicate n x :< x
-
-public export
-lengthOfReplicate : (n : Nat) -> (0 x : a) -> LengthOf (replicate n x)
-lengthOfReplicate 0 x = Z
-lengthOfReplicate (S k) x = S (lengthOfReplicate k x)
diff --git a/src/Inky/Data/SnocList/Elem.idr b/src/Inky/Data/SnocList/Elem.idr
deleted file mode 100644
index c1e69f6..0000000
--- a/src/Inky/Data/SnocList/Elem.idr
+++ /dev/null
@@ -1,116 +0,0 @@
-module Inky.Data.SnocList.Elem
-
-import public Data.SnocList.Elem
-
-import Data.DPair
-import Data.Nat
-import Data.Singleton
-import Inky.Decidable
-import Inky.Decidable.Maybe
-import Inky.Data.Assoc
-import Inky.Data.List
-import Inky.Data.SnocList
-
-export
-Uninhabited (Here {sx, x} ~=~ There {sx = sy, x = z, y} i) where
-  uninhabited Refl impossible
-
-export
-Uninhabited (There {sx = sy, x = z, y} i ~=~ Here {sx, x}) where
-  uninhabited Refl impossible
-
-export
-thereCong :
-  {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j ->
-  There {y = z} i = There {y = z} j
-thereCong Refl = Refl
-
-export
-toNatCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> elemToNat i = elemToNat j
-toNatCong Refl = Refl
-
-export
-thereInjective :
-  {0 i : Elem x sx} -> {0 j : Elem y sx} -> There {y = z} i = There {y = z} j ->
-  i = j
-thereInjective Refl = Refl
-
-export
-toNatInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : elemToNat i = elemToNat j) -> i = j
-toNatInjective {i = Here} {j = Here} prf = Refl
-toNatInjective {i = There i} {j = There j} prf with (toNatInjective {i} {j} $ injective prf)
-  toNatInjective {i = There i} {j = There .(i)} prf | Refl = Refl
-
--- Decidable Equality -----------------------------------------------------------
-
-public export
-reflectEq : (i : Elem x sx) -> (j : Elem y sx) -> (i = j) `When` (elemToNat i == elemToNat j)
-reflectEq Here Here = Refl
-reflectEq Here (There j) = absurd
-reflectEq (There i) Here = absurd
-reflectEq (There i) (There j) = mapWhen thereCong thereInjective $ reflectEq i j
-
-public export
-decEq : (i : Elem x sx) -> (j : Elem y sx) -> Dec' (i = j)
-decEq i j = (elemToNat i == elemToNat j) `Because` reflectEq i j
-
--- Weakening -------------------------------------------------------------------
-
-public export
-wknL : Elem x sx -> LengthOf sy -> Elem x (sx ++ sy)
-wknL pos Z = pos
-wknL pos (S len) = There (wknL pos len)
-
-public export
-wknR : Elem x sx -> Elem x (sy ++ sx)
-wknR Here = Here
-wknR (There pos) = There (wknR pos)
-
-public export
-split : LengthOf sy -> Elem x (sx ++ sy) -> Either (Elem x sx) (Elem x sy)
-split Z pos = Left pos
-split (S len) Here = Right Here
-split (S len) (There pos) = mapSnd There $ split len pos
-
-public export
-wknL' : Elem x sx -> LengthOf xs -> Elem x (sx <>< xs)
-wknL' i Z = i
-wknL' i (S len) = wknL' (There i) len
-
--- Lookup ----------------------------------------------------------------------
-
-export
-nameOf : {sx : SnocList a} -> Elem x sx -> Singleton x
-nameOf Here = Val x
-nameOf (There pos) = nameOf pos
-
--- Search ----------------------------------------------------------------------
-
-export
-lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Elem x sx)
-lookup x [<] = Nothing
-lookup x (sx :< y) =
-  case decEq x y of
-    True `Because` Refl => Just Here
-    False `Because` _ => There <$> lookup x sx
-
-public export
-decLookup : (n : String) -> (sx : SnocList (Assoc a)) -> DecWhen a (\x => Elem (n :- x) sx)
-decLookup n [<] = Nothing `Because` (\_ => absurd)
-decLookup n (sx :< (k :- x)) =
-  map (maybe x id) leftToRight rightToLeft $
-  first (decEq n k) (decLookup n sx)
-  where
-  leftToRight :
-    forall n. (m : Maybe a) ->
-    maybe (n = k) (\y => Elem (n :- y) sx) m ->
-    Elem (n :- maybe x Basics.id m) (sx :< (k :- x))
-  leftToRight Nothing Refl = Here
-  leftToRight (Just _) prf = There prf
-
-  rightToLeft :
-    forall n.
-    (Not (n = k), (y : a) -> Not (Elem (n :- y) sx)) ->
-    (y : a) -> Not (Elem (n :- y) (sx :< (k :- x)))
-  rightToLeft (neq, contra) _ Here = neq Refl
-  rightToLeft (neq, contra) y (There i) = contra y i
diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
deleted file mode 100644
index 886c4e4..0000000
--- a/src/Inky/Data/SnocList/Quantifiers.idr
+++ /dev/null
@@ -1,44 +0,0 @@
-module Inky.Data.SnocList.Quantifiers
-
-import public Data.SnocList.Quantifiers
-
-import Data.List.Quantifiers
-import Inky.Data.SnocList
-import Inky.Data.SnocList.Elem
-import Inky.Decidable
-
-public export
-(<><) : All p xs -> All p sx -> All p (xs <>< sx)
-sxp <>< [] = sxp
-sxp <>< (px :: pxs) = (sxp :< px) <>< pxs
-
-public export
-head : All p (sx :< x) -> p x
-head (prfs :< px) = px
-
-public export
-tail : All p (sx :< x) -> All p sx
-tail (prfs :< px) = prfs
-
-public export
-HSnocList : SnocList Type -> Type
-HSnocList = All id
-
-public export
-all :
-  ((x : a) -> LazyEither (p x) (q x)) ->
-  (sx : SnocList a) -> LazyEither (All p sx) (Any q sx)
-all f [<] = True `Because` [<]
-all f (sx :< x) =
-  map (\prfs => snd prfs :< fst prfs) (either Here There) $
-  both (f x) (all f sx)
-
-public export
-tabulate : LengthOf sx -> (forall x. Elem x sx -> p x) -> All p sx
-tabulate Z f = [<]
-tabulate (S len) f = tabulate len (f . There) :< f Here
-
-public export
-data Pairwise : (a -> a -> Type) -> SnocList a -> Type where
-  Lin : Pairwise r [<]
-  (:<) : Pairwise r sx -> All (flip r x) sx -> Pairwise r (sx :< x)
diff --git a/src/Inky/Data/SnocList/Thinning.idr b/src/Inky/Data/SnocList/Thinning.idr
deleted file mode 100644
index 60666d2..0000000
--- a/src/Inky/Data/SnocList/Thinning.idr
+++ /dev/null
@@ -1,228 +0,0 @@
-module Inky.Data.SnocList.Thinning
-
-import Data.DPair
-import Data.Nat
-import Inky.Data.List
-import Inky.Data.SnocList
-import Inky.Data.SnocList.Var
-import Inky.Data.SnocList.Quantifiers
-import Inky.Decidable.Maybe
-
---------------------------------------------------------------------------------
--- Thinnings -------------------------------------------------------------------
---------------------------------------------------------------------------------
-
-public export
-data Thins : SnocList a -> SnocList a -> Type where
-  Id : sx `Thins` sx
-  Drop : sx `Thins` sy -> sx `Thins` sy :< x
-  Keep : sx `Thins` sy -> sx :< x `Thins` sy :< x
-
-%name Thins f, g, h
-
--- Basics
-
-public export
-indexPos : (f : sx `Thins` sy) -> (pos : Elem x sx) -> Elem x sy
-indexPos Id pos = pos
-indexPos (Drop f) pos = There (indexPos f pos)
-indexPos (Keep f) Here = Here
-indexPos (Keep f) (There pos) = There (indexPos f pos)
-
-public export
-index : (f : sx `Thins` sy) -> Var sx -> Var sy
-index f i = toVar (indexPos f i.pos)
-
-public export
-(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
-Id . g = g
-Drop f . g = Drop (f . g)
-Keep f . Id = Keep f
-Keep f . Drop g = Drop (f . g)
-Keep f . Keep g = Keep (f . g)
-
--- Basic properties
-
-export
-indexPosInjective :
-  (f : sx `Thins` sy) -> {i : Elem x sx} -> {j : Elem y sx} ->
-  (0 _ : elemToNat (indexPos f i) = elemToNat (indexPos f j)) -> i = j
-indexPosInjective Id prf = toNatInjective prf
-indexPosInjective (Drop f) prf = indexPosInjective f (injective prf)
-indexPosInjective (Keep f) {i = Here} {j = Here} prf = Refl
-indexPosInjective (Keep f) {i = There i} {j = There j} prf =
-  thereCong (indexPosInjective f $ injective prf)
-
-export
-indexPosComp :
-  (f : sy `Thins` sz) -> (g : sx `Thins` sy) -> (pos : Elem x sx) ->
-  indexPos (f . g) pos = indexPos f (indexPos g pos)
-indexPosComp Id g pos = Refl
-indexPosComp (Drop f) g pos = cong There (indexPosComp f g pos)
-indexPosComp (Keep f) Id pos = Refl
-indexPosComp (Keep f) (Drop g) pos = cong There (indexPosComp f g pos)
-indexPosComp (Keep f) (Keep g) Here = Refl
-indexPosComp (Keep f) (Keep g) (There pos) = cong There (indexPosComp f g pos)
-
--- Congruence ------------------------------------------------------------------
-
-export
-infix 6 ~~~
-
-public export
-data (~~~) : sx `Thins` sy -> sx `Thins` sz -> Type where
-  IdId : Id ~~~ Id
-  IdKeep : Id ~~~ f -> Id ~~~ Keep f
-  KeepId : f ~~~ Id -> Keep f ~~~ Id
-  DropDrop : f ~~~ g -> Drop f ~~~ Drop g
-  KeepKeep : f ~~~ g -> Keep f ~~~ Keep g
-
-%name Thinning.(~~~) prf
-
-export
-(.indexPos) : f ~~~ g -> (pos : Elem x sx) -> elemToNat (indexPos f pos) = elemToNat (indexPos g pos)
-(IdId).indexPos pos = Refl
-(IdKeep prf).indexPos Here = Refl
-(IdKeep prf).indexPos (There pos) = cong S $ prf.indexPos pos
-(KeepId prf).indexPos Here = Refl
-(KeepId prf).indexPos (There pos) = cong S $ prf.indexPos pos
-(DropDrop prf).indexPos pos = cong S $ prf.indexPos pos
-(KeepKeep prf).indexPos Here = Refl
-(KeepKeep prf).indexPos (There pos) = cong S $ prf.indexPos pos
-
-export
-(.index) :
-  {0 f, g : sx `Thins` sy} -> f ~~~ g -> (i : Var sx) -> index f i = index g i
-prf.index ((%%) n {pos}) = irrelevantEq $ toVarCong $ toNatInjective $ prf.indexPos pos
-
--- Useful for Parsers ----------------------------------------------------------
-
-public export
-(<><) : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 <>< bound `Thins` ctx2 <>< bound
-f <>< Z = f
-f <>< S len = Keep f <>< len
-
-public export
-dropFish : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 `Thins` ctx2 <>< bound
-dropFish f Z = f
-dropFish f (S len) = dropFish (Drop f) len
-
-public export
-dropPos : (pos : Elem x ctx) -> dropElem ctx pos `Thins` ctx
-dropPos Here = Drop Id
-dropPos (There pos) = Keep (dropPos pos)
-
-public export
-dropAll : LengthOf sy -> sx `Thins` sx ++ sy
-dropAll Z = Id
-dropAll (S len) = Drop (dropAll len)
-
-public export
-keepAll : LengthOf sz -> sx `Thins` sy -> sx ++ sz `Thins` sy ++ sz
-keepAll Z f = f
-keepAll (S len) f = Keep (keepAll len f)
-
-public export
-append :
-  sx `Thins` sz -> sy `Thins` sw ->
-  {auto len : LengthOf sw} ->
-  sx ++ sy `Thins` sz ++ sw
-append f Id = keepAll len f
-append f (Drop g) {len = S len} = Drop (append f g)
-append f (Keep g) {len = S len} = Keep (append f g)
-
-public export
-assoc : LengthOf sz -> sx ++ (sy ++ sz) `Thins` (sx ++ sy) ++ sz
-assoc Z = Id
-assoc (S len) = Keep (assoc len)
-
-public export
-growLengthOf : sx `Thins` sy -> LengthOf sx -> LengthOf sy
-growLengthOf Id len = len
-growLengthOf (Drop f) len = S (growLengthOf f len)
-growLengthOf (Keep f) (S len) = S (growLengthOf f len)
-
-public export
-thinLengthOf : sx `Thins` sy -> LengthOf sy -> LengthOf sx
-thinLengthOf Id len = len
-thinLengthOf (Drop f) (S len) = thinLengthOf f len
-thinLengthOf (Keep f) (S len) = S (thinLengthOf f len)
-
-public export
-thinAll : sx `Thins` sy -> All p sy -> All p sx
-thinAll Id env = env
-thinAll (Drop f) (env :< px) = thinAll f env
-thinAll (Keep f) (env :< px) = thinAll f env :< px
-
-public export
-splitL :
-  {0 sx, sy, sz : SnocList a} ->
-  LengthOf sz ->
-  sx `Thins` sy ++ sz ->
-  Exists (\sxA => Exists (\sxB => (sx = sxA ++ sxB, sxA `Thins` sy, sxB `Thins` sz)))
-splitL Z f = Evidence sx (Evidence [<] (Refl, f, Id))
-splitL (S len) Id = Evidence sy (Evidence sz (Refl, Id, Id))
-splitL (S len) (Drop f) =
-  let Evidence sxA (Evidence sxB (Refl, g, h)) = splitL len f in
-  Evidence sxA (Evidence sxB (Refl, g, Drop h))
-splitL (S len) (Keep f) =
-  let Evidence sxA (Evidence sxB (Refl, g, h)) = splitL len f in
-  Evidence sxA (Evidence (sxB :< _) (Refl, g, Keep h))
-
-public export
-splitR :
-  {0 sx, sy, sz : SnocList a} ->
-  LengthOf sy ->
-  sx ++ sy `Thins` sz ->
-  Exists (\sxA => Exists (\sxB => (sz = sxA ++ sxB, sx `Thins` sxA, sy `Thins` sxB)))
-splitR Z f = Evidence sz (Evidence [<] (Refl, f, Id))
-splitR (S len) Id = Evidence sx (Evidence sy (Refl, Id, Id))
-splitR (S len) (Drop f) =
-  let Evidence sxA (Evidence sxB (Refl, g, h)) = splitR (S len) f in
-  Evidence sxA (Evidence (sxB :< _) (Refl, g, Drop h))
-splitR (S len) (Keep f) =
-  let Evidence sxA (Evidence sxB (Refl, g, h)) = splitR len f in
-  Evidence sxA (Evidence (sxB :< _) (Refl, g, Keep h))
-
--- Strengthening ---------------------------------------------------------------
-
-public export
-data Skips : sx `Thins` sy -> Elem y sy -> Type where
-  Here : Drop f `Skips` Here
-  Also : f `Skips` i -> Drop f `Skips` There i
-  There : f `Skips` i -> Keep f `Skips` There i
-
-%name Skips skips
-
-public export
-strengthen :
-  (f : sx `Thins` sy) -> (i : Elem y sy) ->
-  Proof (Elem y sx) (\j => i = indexPos f j) (f `Skips` i)
-strengthen Id i = Just i `Because` Refl
-strengthen (Drop f) Here = Nothing `Because` Here
-strengthen (Drop f) (There i) =
-  map id (\_, prf => cong There prf) Also $
-  strengthen f i
-strengthen (Keep f) Here = Just Here `Because` Refl
-strengthen (Keep f) (There i) =
-  map There (\_, prf => cong There prf) There $
-  strengthen f i
-
-export
-skipsDropPos : (i : Elem x sx) -> dropPos i `Skips` j -> i ~=~ j
-skipsDropPos Here Here = Refl
-skipsDropPos (There i) (There skips) = thereCong (skipsDropPos i skips)
-
------------------------- -------------------------------------------------------
--- Renaming Coalgebras ---------------------------------------------------------
---------------------------------------------------------------------------------
-
-public export
-interface Rename (0 a : Type) (0 t : SnocList a -> Type) where
-  rename :
-    {0 sx, sy : SnocList a} -> sx `Thins` sy ->
-    t sx -> t sy
-  0 renameCong :
-    {0 sx, sy : SnocList a} -> {0 f, g : sx `Thins` sy} -> f ~~~ g ->
-    (x : t sx) -> rename f x = rename g x
-  0 renameId : {0 sx : SnocList a} -> (x : t sx) -> rename Id x = x
diff --git a/src/Inky/Data/SnocList/Var.idr b/src/Inky/Data/SnocList/Var.idr
deleted file mode 100644
index cc7c088..0000000
--- a/src/Inky/Data/SnocList/Var.idr
+++ /dev/null
@@ -1,90 +0,0 @@
-module Inky.Data.SnocList.Var
-
-import public Inky.Data.SnocList.Elem
-
-import Data.Singleton
-import Inky.Data.SnocList
-import Inky.Decidable
-
-export
-prefix 2 %%
-
-public export
-record Var (sx : SnocList a) where
-  constructor (%%)
-  0 name : a
-  {auto pos : Elem name sx}
-
-%name Var i, j, k
-
-public export
-toVar : Elem x sx -> Var sx
-toVar pos = (%%) x {pos}
-
-public export
-ThereVar : Var sx -> Var (sx :< x)
-ThereVar i = toVar (There i.pos)
-
-export
-Show (Var sx) where
-  show i = show (elemToNat i.pos)
-
--- Basic Properties ---------------------------------------------------------
-
-export
-toVarCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> toVar i = toVar j
-toVarCong Refl = Refl
-
-export
-posCong : {0 i, j : Var sx} -> i = j -> i.pos ~=~ j.pos
-posCong Refl = Refl
-
-export
-toVarInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : toVar i = toVar j) -> i = j
-toVarInjective prf = toNatInjective $ toNatCong $ posCong prf
-
-export
-posInjective : {i : Var sx} -> {j : Var sx} -> (0 _ : i.pos ~=~ j.pos) -> i = j
-posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf
-
--- Decidable Equality ----------------------------------------------------------
-
-public export
-DecEq' (Var {a} sx) where
-  does i j = (decEq i.pos j.pos).does
-  reason i j =
-    mapWhen (\prf => irrelevantEq $ posInjective prf) posCong $
-    (decEq i.pos j.pos).reason
-
--- Weakening -------------------------------------------------------------------
-
-public export
-wknL : (len : LengthOf sy) => Var sx -> Var (sx ++ sy)
-wknL i = toVar $ wknL i.pos len
-
-public export
-wknR : Var sx -> Var (sy ++ sx)
-wknR i = toVar $ wknR i.pos
-
-public export
-split : {auto len : LengthOf sy} -> Var (sx ++ sy) -> Either (Var sx) (Var sy)
-split i = bimap toVar toVar $ split len i.pos
-
-public export
-lift1 :
-  (Var sx -> Var sy) ->
-  Var (sx :< x) -> Var (sy :< y)
-lift1 f ((%%) x {pos = Here}) = %% y
-lift1 f ((%%) name {pos = There i}) = ThereVar (f $ %% name)
-
--- Names -----------------------------------------------------------------------
-
-export
-nameOf : {sx : SnocList a} -> (i : Var sx) -> Singleton i.name
-nameOf i = nameOf i.pos
-
--- Search ----------------------------------------------------------------------
-
-export
-lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Var sx)
-lookup x sx = toVar <$> lookup x sx
diff --git a/src/Inky/Data/Thinned.idr b/src/Inky/Data/Thinned.idr
index 6ee0d50..eaf5e7b 100644
--- a/src/Inky/Data/Thinned.idr
+++ b/src/Inky/Data/Thinned.idr
@@ -1,6 +1,6 @@
 module Inky.Data.Thinned
 
-import public Inky.Data.SnocList.Thinning
+import public Flap.Data.SnocList.Thinning
 
 public export
 record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where
@@ -11,8 +11,15 @@ record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where
 
 public export
 rename : (ctx1 `Thins` ctx2) -> Thinned p ctx1 -> Thinned p ctx2
-rename f (value `Over` thins) = value `Over` (f . thins)
+rename f v = v.value `Over` (f . v.thins)
 
 public export
 (.extract) : Rename a p => Thinned p ctx -> p ctx
-(value `Over` thins).extract = rename thins value
+v.extract = rename v.thins v.value
+
+export
+0 extractHomo :
+  Rename a p =>
+  (f : ctx1 `Thins` ctx2) -> (x : Thinned p ctx1) ->
+  rename f x.extract = (rename f x).extract
+extractHomo f x = renameHomo f x.thins x.value
diff --git a/src/Inky/Decidable.idr b/src/Inky/Decidable.idr
deleted file mode 100644
index 7fba676..0000000
--- a/src/Inky/Decidable.idr
+++ /dev/null
@@ -1,261 +0,0 @@
-module Inky.Decidable
-
-import public Inky.Decidable.Either
-
-import Data.Bool
-import Data.Either
-import Data.Maybe
-import Data.List
-import Data.List1
-import Data.List1.Properties
-import Data.Nat
-import Data.SnocList
-import Data.So
-import Data.These
-import Data.Vect
-
-import Decidable.Equality
-
-public export
-When : Type -> Bool -> Type
-When a = Union a (Not a)
-
-public export
-Dec' : (0 _ : Type) -> Type
-Dec' a = LazyEither a (Not a)
-
--- Operations ------------------------------------------------------------------
-
--- Conversion to Dec
-
-public export
-fromDec : Dec a -> Dec' a
-fromDec (Yes prf) = True `Because` prf
-fromDec (No contra) = False `Because` contra
-
-public export
-toDec : Dec' a -> Dec a
-toDec (True `Because` prf) = Yes prf
-toDec (False `Because` contra) = No contra
-
--- Negation
-
-public export
-notWhen : {b : Bool} -> a `When` b -> Not a `When` not b
-notWhen = Union.map id (\prf, contra => contra prf) . Union.not
-
-public export
-notDec : Dec' a -> Dec' (Not a)
-notDec p = not p.does `Because` notWhen p.reason
-
--- Maps
-
-public export
-mapWhen : (a -> a') -> (0 _ : a' -> a) -> {b : Bool} -> a `When` b -> a' `When` b
-mapWhen f g = Union.map f (\contra, prf => void $ contra $ g prf)
-
-public export
-mapDec : (a -> b) -> (0 _ : b -> a) -> Dec' a -> Dec' b
-mapDec f g = map f (\contra, prf => void $ contra $ g prf)
-
--- Conjunction
-
-public export
-andWhen : {b1, b2 :  Bool} -> a1 `When` b1 -> Lazy (a2 `When` b2) -> (a1, a2) `When` (b1 && b2)
-andWhen x y =
-  Union.map {d = Not (a1, a2)} id (\x, (y, z) => either (\f => f y) (\g => g z) x) $
-  Union.both x y
-
-public export
-andDec : Dec' a -> Dec' b -> Dec' (a, b)
-andDec p q = (p.does && q.does) `Because` andWhen p.reason q.reason
-
--- Disjunction
-
-public export
-elseWhen : {b1, b2 : Bool} -> a1 `When` b1 -> Lazy (a2 `When` b2) -> Either a1 a2 `When` (b1 || b2)
-elseWhen x y =
-  Union.map {b = (Not a1, Not a2)} id (\(f, g) => either f g) $
-  Union.first x y
-
-public export
-elseDec : Dec' a -> Dec' b -> Dec' (Either a b)
-elseDec p q = (p.does || q.does) `Because` elseWhen p.reason q.reason
-
-public export
-orWhen : {b1, b2 : Bool} -> a1 `When` b1 -> a2 `When` b2 -> These a1 a2 `When` (b1 || b2)
-orWhen x y =
-  Union.map {b = (Not a1, Not a2)} id (\(f, g) => these f g (const g)) $
-  Union.any x y
-
-public export
-orDec : Dec' a -> Dec' b -> Dec' (These a b)
-orDec p q = (p.does || q.does) `Because` orWhen p.reason q.reason
-
--- Dependent Versions
-
-public export
-thenDec :
-  (0 b : a -> Type) ->
-  (0 unique : (x, y : a) -> b x -> b y) ->
-  Dec' a -> ((x : a) -> Dec' (b x)) -> Dec' (x ** b x)
-thenDec b unique p f =
-  map id
-    (\contra, (x ** prf) =>
-      either
-        (\contra => contra x)
-        (\yContra => void $ snd yContra $ unique x (fst yContra) prf)
-        contra) $
-  andThen p f
-
--- Equality --------------------------------------------------------------------
-
-public export
-interface DecEq' (0 a : Type) where
-  does : (x, y : a) -> Bool
-  reason : (x, y : a) -> (x = y) `When` (does x y)
-
-  decEq : (x, y : a) -> Dec' (x = y)
-  decEq x y = does x y `Because` reason x y
-
-public export
-whenCong : (0 _ : Injective f) => {b : Bool} -> (x = y) `When` b -> (f x = f y) `When` b
-whenCong = mapWhen (\prf => cong f prf) (\prf => inj f prf)
-
-public export
-whenCong2 :
-  (0 _ : Biinjective f) =>
-  {b1, b2 : Bool} ->
-  (x = y) `When` b1 -> (z = w) `When` b2 ->
-  (f x z = f y w) `When` (b1 && b2)
-whenCong2 p q =
-  mapWhen {a = (_, _)} (\prfs => cong2 f (fst prfs) (snd prfs)) (\prf => biinj f prf) $
-  andWhen p q
-
-[ToEq] DecEq' a => Eq a where
-  x == y = does x y
-
--- Instances -------------------------------------------------------------------
-
-public export
-DecEq' () where
-  does _ _ = True
-  reason () () = Refl
-
-public export
-DecEq' Bool where
-  does b1 b2 = b1 == b2
-
-  reason False False = Refl
-  reason False True = absurd
-  reason True False = absurd
-  reason True True = Refl
-
-public export
-DecEq' Nat where
-  does k n = k == n
-
-  reason 0 0 = Refl
-  reason 0 (S n) = absurd
-  reason (S k) 0 = absurd
-  reason (S k) (S n) = whenCong (reason k n)
-
-public export
-(d : DecEq' a) => DecEq' (Maybe a) where
-  does x y = let _ = ToEq @{d} in x == y
-
-  reason Nothing Nothing = Refl
-  reason Nothing (Just y) = absurd
-  reason (Just x) Nothing = absurd
-  reason (Just x) (Just y) = whenCong (reason x y)
-
-public export
-(d1 : DecEq' a) => (d2 : DecEq' b) => DecEq' (Either a b) where
-  does x y = let _ = ToEq @{d1} in let _ = ToEq @{d2} in x == y
-
-  reason (Left x) (Left y) = whenCong (reason x y)
-  reason (Left x) (Right y) = absurd
-  reason (Right x) (Left y) = absurd
-  reason (Right x) (Right y) = whenCong (reason x y)
-
-
-public export
-(d1 : DecEq' a) => (d2 : DecEq' b) => DecEq' (These a b) where
-  does x y = let _ = ToEq @{d1} in let _ = ToEq @{d2} in x == y
-
-  reason (This x) (This y) = whenCong (reason x y)
-  reason (That x) (That y) = whenCong (reason x y)
-  reason (Both x z) (Both y w) = whenCong2 (reason x y) (reason z w)
-  reason (This x) (That y) = \case Refl impossible
-  reason (This x) (Both y z) = \case Refl impossible
-  reason (That x) (This y) = \case Refl impossible
-  reason (That x) (Both y z) = \case Refl impossible
-  reason (Both x z) (This y) = \case Refl impossible
-  reason (Both x z) (That y) = \case Refl impossible
-
-public export
-(d1 : DecEq' a) => (d2 : DecEq' b) => DecEq' (a, b) where
-  does x y = let _ = ToEq @{d1} in let _ = ToEq @{d2} in x == y
-
-  reason (x, y) (z, w) = whenCong2 (reason x z) (reason y w)
-
-public export
-(d : DecEq' a) => DecEq' (List a) where
-  does x y = let _ = ToEq @{d} in x == y
-
-  reason [] [] = Refl
-  reason [] (y :: ys) = absurd
-  reason (x :: xs) [] = absurd
-  reason (x :: xs) (y :: ys) = whenCong2 (reason x y) (reason xs ys)
-
-public export
-(d : DecEq' a) => DecEq' (List1 a) where
-  does x y = let _ = ToEq @{d} in x == y
-
-  reason (x ::: xs) (y ::: ys) = whenCong2 (reason x y) (reason xs ys)
-
-public export
-(d : DecEq' a) => DecEq' (SnocList a) where
-  does x y = let _ = ToEq @{d} in x == y
-
-  reason [<] [<] = Refl
-  reason [<] (sy :< y) = absurd
-  reason (sx :< x) [<] = absurd
-  reason (sx :< x) (sy :< y) =
-    rewrite sym $ andCommutative (does sx sy) (does x y) in
-    whenCong2 (reason sx sy) (reason x y)
-
--- Other Primitives
-
-%unsafe
-public export
-primitiveEq : Eq a => (x, y : a) -> (x = y) `When` (x == y)
-primitiveEq x y with (x == y)
-  _ | True = believe_me (Refl {x})
-  _ | False = \prf => believe_me {b = Void} ()
-
-%unsafe
-public export
-[FromEq] Eq a => DecEq' a where
-  does x y = x == y
-  reason x y = primitiveEq x y
-
-public export
-DecEq' Int where
-  does = does @{FromEq}
-  reason = reason @{FromEq}
-
-public export
-DecEq' Char where
-  does = does @{FromEq}
-  reason = reason @{FromEq}
-
-public export
-DecEq' Integer where
-  does = does @{FromEq}
-  reason = reason @{FromEq}
-
-public export
-DecEq' String where
-  does = does @{FromEq}
-  reason = reason @{FromEq}
diff --git a/src/Inky/Decidable/Either.idr b/src/Inky/Decidable/Either.idr
deleted file mode 100644
index bea3364..0000000
--- a/src/Inky/Decidable/Either.idr
+++ /dev/null
@@ -1,111 +0,0 @@
-module Inky.Decidable.Either
-
-import Data.So
-import Data.These
-
-public export
-Union : Type -> Type -> Bool -> Type
-Union a b False = b
-Union a b True = a
-
-public export
-record LazyEither (0 a, b : Type) where
-  constructor Because
-  does : Bool
-  reason : Lazy (Union a b does)
-
-%name LazyEither p, q
-
-namespace Union
-  public export
-  map : {tag : Bool} -> (a -> c) -> (b -> d) -> Union a b tag -> Union c d tag
-  map {tag = False} f g x = g x
-  map {tag = True} f g x = f x
-
-  public export
-  not : {tag : Bool} -> Union a b tag -> Union b a (not tag)
-  not {tag = False} x = x
-  not {tag = True} x = x
-
-  public export
-  both :
-    {tag1 : Bool} -> {tag2 : Lazy Bool} ->
-    Union a b tag1 -> Lazy (Union c d tag2) ->
-    Union (a, c) (Either b d) (tag1 && tag2)
-  both {tag1 = True, tag2 = True} x y = (x, y)
-  both {tag1 = True, tag2 = False} x y = Right y
-  both {tag1 = False} x y = Left x
-
-  public export
-  first :
-    {tag1 : Bool} -> {tag2 : Lazy Bool} ->
-    Union a b tag1 -> Lazy (Union c d tag2) ->
-    Union (Either a c) (b, d) (tag1 || tag2)
-  first {tag1 = True} x y = Left x
-  first {tag1 = False, tag2 = True} x y = Right y
-  first {tag1 = False, tag2 = False} x y = (x, y)
-
-  public export
-  all :
-    {tag1, tag2 : Bool} ->
-    Union a b tag1 -> Union c d tag2 ->
-    Union (a, c) (These b d) (tag1 && tag2)
-  all {tag1 = True, tag2 = True} x y = (x, y)
-  all {tag1 = True, tag2 = False} x y = That y
-  all {tag1 = False, tag2 = True} x y = This x
-  all {tag1 = False, tag2 = False} x y = Both x y
-
-  public export
-  any :
-    {tag1, tag2 : Bool} ->
-    Union a b tag1 -> Union c d tag2 ->
-    Union (These a c) (b, d) (tag1 || tag2)
-  any {tag1 = True, tag2 = True} x y = Both x y
-  any {tag1 = True, tag2 = False} x y = This x
-  any {tag1 = False, tag2 = True} x y = That y
-  any {tag1 = False, tag2 = False} x y = (x, y)
-
-public export
-map : (a -> c) -> (b -> d) -> LazyEither a b -> LazyEither c d
-map f g p = p.does `Because` Union.map f g p.reason
-
-public export
-not : LazyEither a b -> LazyEither b a
-not p = not p.does `Because` Union.not p.reason
-
-public export
-both : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (a, c) (Either b d)
-both p q = p.does && q.does `Because` Union.both p.reason q.reason
-
-public export
-first : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (Either a c) (b, d)
-first p q = p.does || q.does `Because` Union.first p.reason q.reason
-
-public export
-all : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (a, c) (These b d)
-all p q = p.does && q.does `Because` Union.all p.reason q.reason
-
-public export
-any : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (These a c) (b, d)
-any p q = p.does || q.does `Because` Union.any p.reason q.reason
-
-public export
-so : (b : Bool) -> LazyEither (So b) (So $ not b)
-so b = b `Because` if b then Oh else Oh
-
-export autobind infixr 0 >=>
-
-public export
-andThen :
-  {0 p, q : a -> Type} ->
-  LazyEither a b -> ((x : a) -> LazyEither (p x) (q x)) ->
-  LazyEither (x ** p x) (Either b (x ** q x))
-andThen (True `Because` x) f = map (\px => (x ** px)) (\qx => Right (x ** qx)) (f x)
-andThen (False `Because` y) f = False `Because` (Left y)
-
-public export
-(>=>) :
-  {0 p, q : a -> Type} ->
-  LazyEither a b -> ((x : a) -> LazyEither (p x) (q x)) ->
-  LazyEither (x ** p x) (Either b (x ** q x))
-(>=>) = andThen
diff --git a/src/Inky/Decidable/Maybe.idr b/src/Inky/Decidable/Maybe.idr
deleted file mode 100644
index 2f1d83c..0000000
--- a/src/Inky/Decidable/Maybe.idr
+++ /dev/null
@@ -1,146 +0,0 @@
-module Inky.Decidable.Maybe
-
-import Data.Maybe
-import Data.These
-import Inky.Decidable.Either
-
-public export
-WhenJust : (a -> Type) -> Type -> Maybe a -> Type
-WhenJust p b (Just x) = p x
-WhenJust p b Nothing = b
-
-public export
-record Proof (0 a : Type) (0 p : a -> Type) (0 b : Type) where
-  constructor Because
-  does : Maybe a
-  reason : WhenJust p b does
-
-%name Proof p, q
-
-public export
-DecWhen : (0 a : Type) -> (0 p : a -> Type) -> Type
-DecWhen a p = Proof a p ((x : a) -> Not (p x))
-
--- Operations ------------------------------------------------------------------
-
-public export
-(.forget) : Proof a p b -> LazyEither (x ** p x) b
-(Just x `Because` px).forget = True `Because` (x ** px)
-(Nothing `Because` y).forget = False `Because` y
-
-public export
-map :
-  (f : a -> a') ->
-  ((x : a) -> p x -> q (f x)) ->
-  (b -> b') ->
-  Proof a p b -> Proof a' q b'
-map f g h (Just x `Because` px) = Just (f x) `Because` g x px
-map f g h (Nothing `Because` y) = Nothing `Because` h y
-
-export autobind infixr 0 >=>
-
-public export
-andThen :
-  {0 q : a -> a' -> Type} ->
-  {0 b' : a -> Type} ->
-  Proof a p b ->
-  ((x : a) -> Proof a' (q x) (b' x)) ->
-  Proof (a, a') (\xy => (p (fst xy), uncurry q xy)) (Either b (x ** (p x, b' x)))
-andThen (Just x `Because` px) f = map (x,) (\_ => (px,)) (\y => Right (x ** (px, y))) $ f x
-andThen (Nothing `Because` y) f = Nothing `Because` Left y
-
-public export
-(>=>) :
-  {0 q : a -> a' -> Type} ->
-  {0 b' : a -> Type} ->
-  Proof a p b ->
-  ((x : a) -> Proof a' (q x) (b' x)) ->
-  Proof (a, a') (\xy => (p (fst xy), uncurry q xy)) (Either b (x ** (p x, b' x)))
-(>=>) = andThen
-
-public export
-andThen' :
-  {0 a' : a -> Type} ->
-  {0 q : (x : a) -> a' x -> Type} ->
-  {0 b' : a -> Type} ->
-  Proof a p b ->
-  ((x : a) -> Proof (a' x) (q x) (b' x)) ->
-  Proof (x ** a' x) (\xy => (p (fst xy), q (fst xy) (snd xy))) (Either b (x ** (p x, b' x)))
-andThen' (Just x `Because` px) f =
-  map (\y => (x ** y)) (\_ => (px,)) (\y => Right (x ** (px, y))) $ f x
-andThen' (Nothing `Because` y) f = Nothing `Because` Left y
-
-public export
-all :
-  Proof a p b ->
-  Proof a' q b' ->
-  Proof (a, a') (\xy => (p (fst xy), q (snd xy))) (These b b')
-all (Just x `Because` px) (Just y `Because` py) = Just (x, y) `Because` (px, py)
-all (Just x `Because` px) (Nothing `Because` y) = Nothing `Because` That y
-all (Nothing `Because` x) q =
-  Nothing `Because`
-    case q of
-      (Just _ `Because` _) => This x
-      (Nothing `Because` y) => Both x y
-
-public export
-first :
-  Proof a p b ->
-  Lazy (Proof c q d) ->
-  Proof (Either a c) (either p q) (b, d)
-first (Just x `Because` px) q = Just (Left x) `Because` px
-first (Nothing `Because` x) (Just y `Because` py) = Just (Right y) `Because` py
-first (Nothing `Because` x) (Nothing `Because` y) = Nothing `Because` (x, y)
-
-namespace Either
-  public export
-  andThen :
-    (0 c : a -> Type) ->
-    (0 p : (x : a) -> c x -> Type) ->
-    (0 d : a -> Type) ->
-    LazyEither a b -> ((x : a) -> Proof (c x) (p x) (d x)) ->
-    Proof (x ** c x) (\xy => p (fst xy) (snd xy)) (Either b (x ** d x))
-  andThen _ _ _ (True `Because` x) f = map (\y => (x ** y)) (\_ => id) (\y => Right (x ** y)) (f x)
-  andThen _ _ _ (False `Because` y) f = Nothing `Because` Left y
-
-  public export
-  first :
-    LazyEither a b ->
-    Lazy (Proof c p d) ->
-    Proof (Maybe c) (maybe a p) (b, d)
-  first (True `Because` x) q = Just Nothing `Because` x
-  first (False `Because` x) (Just y `Because` py) = Just (Just y) `Because` py
-  first (False `Because` x) (Nothing `Because` y) = Nothing `Because` (x, y)
-
-  public export
-  all : LazyEither a b -> Lazy (Proof c p d) -> Proof c (\x => (a, p x)) (These b d)
-  all (True `Because` x) (Just y `Because` py) = Just y `Because` (x, py)
-  all (True `Because` x) (Nothing `Because` y) = Nothing `Because` That y
-  all (False `Because` x) q =
-    Nothing `Because`
-      case q of
-        (Just y `Because` _) => This x
-        (Nothing `Because` y) => Both x y
-
-namespace Elim
-  export autobind infixr 0 >=>
-
-  public export
-  andThen :
-    {0 q, r : a -> Type} ->
-    Proof a p b -> ((x : a) -> LazyEither (q x) (r x)) ->
-    LazyEither (x ** (p x, q x)) (Either b (x ** (p x, r x)))
-  andThen (Just x `Because` px) f = map (\qx => (x ** (px, qx))) (\rx => Right (x ** (px, rx))) (f x)
-  andThen (Nothing `Because` y) f = False `Because` Left y
-
-  public export
-  (>=>) :
-    {0 q, r : a -> Type} ->
-    Proof a p b -> ((x : a) -> LazyEither (q x) (r x)) ->
-    LazyEither (x ** (p x, q x)) (Either b (x ** (p x, r x)))
-  (>=>) = andThen
-
-public export
-pure : (x : a) -> LazyEither (b x) c -> Proof a b c
-pure x (True `Because` y) = Just x `Because` y
-pure x (False `Because` y) = Nothing `Because` y
diff --git a/src/Inky/Parser.idr b/src/Inky/Parser.idr
deleted file mode 100644
index 94d8eb8..0000000
--- a/src/Inky/Parser.idr
+++ /dev/null
@@ -1,733 +0,0 @@
-module Inky.Parser
-
-import public Data.List.Quantifiers
-
-import Control.WellFounded
-import Data.Bool
-import Data.DPair
-import Data.List
-import Data.List1
-import Data.Nat
-import Data.So
-import Data.String.Extra
-import Inky.Data.Context
-import Inky.Data.Context.Var
-import Inky.Data.SnocList.Quantifiers
-import Inky.Data.SnocList.Thinning
-import Text.Lexer
-
-export
-Interpolation Bounds where
-  interpolate bounds = "\{show (1 + bounds.startLine)}:\{show bounds.startCol}--\{show (1 + bounds.endLine)}:\{show bounds.endCol}"
-
--- Parser Expressions ----------------------------------------------------------
-
-export infixl 3 <**>, **>, <**
-export infixr 2 <||>
-
-public export
-linUnless : Bool -> Context a -> Context a
-linUnless False ctx = [<]
-linUnless True ctx = ctx
-
-public export
-linUnlessLin : (0 a : Type) -> (b : Bool) -> linUnless {a} b [<] = [<]
-linUnlessLin a False = Refl
-linUnlessLin a True = Refl
-
-public export
-data Parser : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> Type -> Type
-
-public export
-data ParserChain : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> List Type -> Type
-
-data Parser where
-  Var : Var free (nil, a) -> Parser i nil locked free a
-  Lit : (text : i) -> Parser i False locked free String
-  Seq :
-    ParserChain i nil locked free as ->
-    Parser i nil locked free (HList as)
-  OneOf :
-    {nils : List Bool} ->
-    All (\nil => Parser i nil locked free a) nils ->
-    {auto 0 prf : length (filter Basics.id nils) `LTE` 1} ->
-    Parser i (any Basics.id nils) locked free a
-  Fix :
-    (0 x : String) ->
-    Parser i nil (locked :< (x :- (nil, a))) free a ->
-    Parser i nil locked free a
-  Map : (a -> b) -> Parser i nil locked free a -> Parser i nil locked free b
-  WithBounds : Parser i nil locked free a -> Parser i nil locked free (WithBounds a)
-
-data ParserChain where
-  Nil : ParserChain i True locked free []
-  (::) :
-    {nil1, nil2 : Bool} ->
-    Parser i nil1 locked free a ->
-    ParserChain i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) as ->
-    ParserChain i (nil1 && nil2) locked free (a :: as)
-
-%name Parser p, q
-%name ParserChain ps, qs
-
--- Weakening -------------------------------------------------------------------
-
-public export
-rename :
-  locked1 `Thins` locked2 ->
-  free1 `Thins` free2 ->
-  {auto len : LengthOf locked2} ->
-  Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a
-public export
-renameChain :
-  locked1 `Thins` locked2 ->
-  free1 `Thins` free2 ->
-  {auto len : LengthOf locked2} ->
-  ParserChain i nil locked1 free1 a -> ParserChain i nil locked2 free2 a
-public export
-renameAll :
-  locked1 `Thins` locked2 ->
-  free1 `Thins` free2 ->
-  {auto len : LengthOf locked2} ->
-  {0 nils : List Bool} ->
-  All (\nil => Parser i nil locked1 free1 a) nils ->
-  All (\nil => Parser i nil locked2 free2 a) nils
-
-rename f g (Var i) = Var (toVar $ indexPos g i.pos)
-rename f g (Lit text) = Lit text
-rename f g (Seq ps) = Seq (renameChain f g ps)
-rename f g (OneOf ps) = OneOf (renameAll f g ps)
-rename f g (Fix x p) = Fix x (rename (Keep f) g p)
-rename f g (Map h p) = Map h (rename f g p)
-rename f g (WithBounds p) = WithBounds (rename f g p)
-
-renameChain f g [] = []
-renameChain f g ((::) {nil1 = False} p ps) = rename f g p :: renameChain Id (append g f) ps
-renameChain f g ((::) {nil1 = True} p ps) = rename f g p :: renameChain f g ps
-
-renameAll f g [] = []
-renameAll f g (p :: ps) = rename f g p :: renameAll f g ps
-
-public export
-weaken :
-  (len1 : LengthOf free2) ->
-  {auto len2 : LengthOf locked} ->
-  Parser i nil (free2 ++ locked) free1 a -> Parser i nil locked (free1 ++ free2) a
-public export
-weakenChain :
-  (len1 : LengthOf free2) ->
-  {auto len2 : LengthOf locked} ->
-  ParserChain i nil (free2 ++ locked) free1 a -> ParserChain i nil locked (free1 ++ free2) a
-public export
-weakenAll :
-  (len1 : LengthOf free2) ->
-  {auto len2 : LengthOf locked} ->
-  {0 nils : List Bool} ->
-  All (\nil => Parser i nil (free2 ++ locked) free1 a) nils ->
-  All (\nil => Parser i nil locked (free1 ++ free2) a) nils
-
-weaken len1 (Var x) = Var (wknL x)
-weaken len1 (Lit text) = Lit text
-weaken len1 (Seq ps) = Seq (weakenChain len1 ps)
-weaken len1 (OneOf ps) = OneOf (weakenAll len1 ps)
-weaken len1 (Fix x p) = Fix x (weaken len1 p)
-weaken len1 (Map f p) = Map f (weaken len1 p)
-weaken len1 (WithBounds p) = WithBounds (weaken len1 p)
-
-weakenChain len1 [] = []
-weakenChain len1 ((::) {nil1 = False} p ps) = weaken len1 p :: renameChain Id (assoc len2) ps
-weakenChain len1 ((::) {nil1 = True} p ps) = weaken len1 p :: weakenChain len1 ps
-
-weakenAll len1 [] = []
-weakenAll len1 (p :: ps) = weaken len1 p :: weakenAll len1 ps
-
--- Substitution ----------------------------------------------------------------
-
-public export
-sub :
-  {auto len : LengthOf locked2} ->
-  (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) ->
-  (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) ->
-  Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a
-public export
-subChain :
-  {auto len : LengthOf locked2} ->
-  (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) ->
-  (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) ->
-  ParserChain i nil locked1 free1 a -> ParserChain i nil locked2 free2 a
-public export
-subAll :
-  {auto len : LengthOf locked2} ->
-  (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) ->
-  (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) ->
-  {0 nils : List Bool} ->
-  All (\nil => Parser i nil locked1 free1 a) nils -> All (\nil => Parser i nil locked2 free2 a) nils
-
-sub f g (Var x) = (indexAll x.pos g).value
-sub f g (Lit text) = Lit text
-sub f g (Seq ps) = Seq (subChain f g ps)
-sub f g (OneOf ps) = OneOf (subAll f g ps)
-sub f g (Fix x p) =
-  Fix x $
-  sub
-    (mapProperty (map $ rename Id (Drop Id)) f :< (x :- Var (%%% x)))
-    (mapProperty (map $ rename (Drop Id) Id) g)
-    p
-sub f g (Map h p) = Map h (sub f g p)
-sub f g (WithBounds p) = WithBounds (sub f g p)
-
-subChain f g [] = []
-subChain f g ((::) {nil1 = False} p ps) =
-  sub f g p ::
-  subChain [<] (mapProperty (map $ weaken len) g ++ f) ps
-subChain f g ((::) {nil1 = True} p ps) = sub f g p :: subChain f g ps
-
-subAll f g [] = []
-subAll f g (p :: ps) = sub f g p :: subAll f g ps
-
--- Typing ----------------------------------------------------------------------
-
--- Lists are sufficient, as we assume each symbol appears once.
--- TODO: switch to some efficient tree?
-
-public export
-peek :
-  (env : All (Assoc0 $ const $ List i) free) ->
-  Parser i nil locked free a -> List i
-public export
-peekChain :
-  (env : All (Assoc0 $ const $ List i) free) ->
-  ParserChain i nil locked free a -> List i
-public export
-peekAll :
-  (env : All (Assoc0 $ const $ List i) free) ->
-  {0 nils : List Bool} ->
-  All (\nil => Parser i nil locked free a) nils ->
-  All (const $ List i) nils
-
-peek env (Var x) = (indexAll x.pos env).value
-peek env (Lit text) = [text]
-peek env (Seq ps) = peekChain env ps
-peek env (OneOf ps) = concat (forget $ peekAll env ps)
-peek env (Fix x p) = peek env p
-peek env (Map f p) = peek env p
-peek env (WithBounds p) = peek env p
-
-peekChain env [] = []
-peekChain env ((::) {nil1 = False} p ps) = peek env p
-peekChain env ((::) {nil1 = True} p ps) = peek env p ++ peekChain env ps
-
-peekAll env [] = []
-peekAll env (p :: ps) = peek env p :: peekAll env ps
-
-public export
-follow :
-  (penv1 : All (Assoc0 $ const $ List i) locked) ->
-  (penv2 : All (Assoc0 $ const $ List i) free) ->
-  (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-  (fenv2 : All (Assoc0 $ const $ List i) free) ->
-  Parser i nil locked free a -> List i
-public export
-followChain :
-  (penv1 : All (Assoc0 $ const $ List i) locked) ->
-  (penv2 : All (Assoc0 $ const $ List i) free) ->
-  (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-  (fenv2 : All (Assoc0 $ const $ List i) free) ->
-  ParserChain i nil locked free a -> List i
-public export
-followAll :
-  (penv1 : All (Assoc0 $ const $ List i) locked) ->
-  (penv2 : All (Assoc0 $ const $ List i) free) ->
-  (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-  (fenv2 : All (Assoc0 $ const $ List i) free) ->
-  {0 nils : List Bool} ->
-  All (\nil => Parser i nil locked free a) nils ->
-  List i
-
-follow penv1 penv2 fenv1 fenv2 (Var x) = (indexAll x.pos fenv2).value
-follow penv1 penv2 fenv1 fenv2 (Lit text) = []
-follow penv1 penv2 fenv1 fenv2 (Seq ps) = followChain penv1 penv2 fenv1 fenv2 ps
-follow penv1 penv2 fenv1 fenv2 (OneOf ps) = followAll penv1 penv2 fenv1 fenv2 ps
-follow penv1 penv2 fenv1 fenv2 (Fix x p) =
-  -- Conjecture: The fix point converges after one step
-  -- Proof:
-  --   - we always add information
-  --   - no step depends on existing information
-  follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- empty)) fenv2 p
-follow penv1 penv2 fenv1 fenv2 (Map f p) = follow penv1 penv2 fenv1 fenv2 p
-follow penv1 penv2 fenv1 fenv2 (WithBounds p) = follow penv1 penv2 fenv1 fenv2 p
-
-followChain penv1 penv2 fenv1 fenv2 [] = []
-followChain penv1 penv2 fenv1 fenv2 ((::) {nil1 = False, nil2} p ps) =
-  (if nil2
-  then peekChain (penv2 ++ penv1) ps ++ follow penv1 penv2 fenv1 fenv2 p
-  else []) ++
-  followChain [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ps
-followChain penv1 penv2 fenv1 fenv2 ((::) {nil1 = True, nil2} p ps) =
-  (if nil2
-  then peekChain penv2 ps ++ follow penv1 penv2 fenv1 fenv2 p
-  else []) ++
-  followChain penv1 penv2 fenv1 fenv2 ps
-
-followAll penv1 penv2 fenv1 fenv2 [] = []
-followAll penv1 penv2 fenv1 fenv2 (p :: ps) =
-  follow penv1 penv2 fenv1 fenv2 p ++
-  followAll penv1 penv2 fenv1 fenv2 ps
-
-public export
-all' : (a -> Bool) -> List a -> Bool
-all' f [] = True
-all' f (x :: xs) = f x && all' f xs
-
-allTrue : (xs : List a) -> all' (const True) xs = True
-allTrue [] = Refl
-allTrue (x :: xs) = allTrue xs
-
-public export
-disjoint : Eq a => List (List a) -> Bool
-disjoint [] = True
-disjoint (xs :: xss) = all' (\ys => all' (\x => not (x `elem` ys)) xs) xss && disjoint xss
-
-namespace WellTyped
-  public export
-  wellTyped :
-    (e : Eq i) ->
-    (penv1 : All (Assoc0 $ const $ List i) locked) ->
-    (penv2 : All (Assoc0 $ const $ List i) free) ->
-    (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-    (fenv2 : All (Assoc0 $ const $ List i) free) ->
-    Parser i nil locked free a ->
-    Bool
-  public export
-  wellTypedChain :
-    (e : Eq i) ->
-    (penv1 : All (Assoc0 $ const $ List i) locked) ->
-    (penv2 : All (Assoc0 $ const $ List i) free) ->
-    (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-    (fenv2 : All (Assoc0 $ const $ List i) free) ->
-    ParserChain i nil locked free a ->
-    Bool
-  public export
-  allWellTyped :
-    (e : Eq i) ->
-    (penv1 : All (Assoc0 $ const $ List i) locked) ->
-    (penv2 : All (Assoc0 $ const $ List i) free) ->
-    (fenv1 : All (Assoc0 $ const $ List i) locked) ->
-    (fenv2 : All (Assoc0 $ const $ List i) free) ->
-    {0 nils : List Bool} ->
-    All (\nil => Parser i nil locked free a) nils ->
-    Bool
-
-  wellTyped e penv1 penv2 fenv1 fenv2 (Var i) = True
-  wellTyped e penv1 penv2 fenv1 fenv2 (Lit txt) = True
-  wellTyped e penv1 penv2 fenv1 fenv2 (Seq ps) = wellTypedChain e penv1 penv2 fenv1 fenv2 ps
-  wellTyped e penv1 penv2 fenv1 fenv2 (OneOf {nils, prf} ps) =
-    disjoint (forget $ peekAll penv2 ps) && allWellTyped e penv1 penv2 fenv1 fenv2 ps
-  wellTyped e penv1 penv2 fenv1 fenv2 (Fix x p) =
-    wellTyped e
-      (penv1 :< (x :- peek penv2 p))
-      penv2
-      (fenv1 :< (x :- follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- [])) fenv2 p))
-      fenv2
-      p
-  wellTyped e penv1 penv2 fenv1 fenv2 (Map f p) = wellTyped e penv1 penv2 fenv1 fenv2 p
-  wellTyped e penv1 penv2 fenv1 fenv2 (WithBounds p) = wellTyped e penv1 penv2 fenv1 fenv2 p
-
-  wellTypedChain e penv1 penv2 fenv1 fenv2 [] = True
-  wellTypedChain e penv1 penv2 fenv1 fenv2 ((::) {nil1 = False} p ps) =
-    disjoint [follow penv1 penv2 fenv1 fenv2 p, peekChain (penv2 ++ penv1) ps] &&
-    wellTyped e penv1 penv2 fenv1 fenv2 p &&
-    wellTypedChain e [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ps
-  wellTypedChain e penv1 penv2 fenv1 fenv2 ((::) {nil1 = True} p ps) =
-    disjoint [follow penv1 penv2 fenv1 fenv2 p, peekChain penv2 ps] &&
-    wellTyped e penv1 penv2 fenv1 fenv2 p &&
-    wellTypedChain e penv1 penv2 fenv1 fenv2 ps
-
-  allWellTyped e penv1 penv2 fenv1 fenv2 [] = True
-  allWellTyped e penv1 penv2 fenv1 fenv2 (p :: ps) =
-    wellTyped e penv1 penv2 fenv1 fenv2 p &&
-    allWellTyped e penv1 penv2 fenv1 fenv2 ps
-
--- Parsing Function ------------------------------------------------------------
-
--- Utilty for recursion
-
-public export
-data SmallerX : Bool -> List a -> List a -> Type where
-  Strict : {0 xs, ys : List a} -> xs `Smaller` ys -> SmallerX False xs ys
-  Lax : {0 xs, ys : List a} -> size xs `LTE` size ys -> SmallerX True xs ys
-
-transX :
-  {xs, ys, zs : List a} ->
-  SmallerX b1 xs ys -> SmallerX b2 ys zs -> SmallerX (b1 && b2) xs zs
-transX (Strict prf1) (Strict prf2) = Strict (transitive prf1 (lteSuccLeft prf2))
-transX (Strict prf1) (Lax prf2) = Strict (transitive prf1 prf2)
-transX (Lax prf1) (Strict prf2) = Strict (transitive (LTESucc prf1) prf2)
-transX (Lax prf1) (Lax prf2) = Lax (transitive prf1 prf2)
-
-ofSmaller : {b : Bool} -> {0 xs, ys : List a} -> xs `Smaller` ys -> SmallerX b xs ys
-ofSmaller {b = False} prf = Strict prf
-ofSmaller {b = True} prf = Lax (lteSuccLeft prf)
-
-wknSmallerL : SmallerX b1 xs ys -> (b2 : Bool) -> SmallerX (b1 || b2) xs ys
-wknSmallerL (Strict prf) _ = ofSmaller prf
-wknSmallerL (Lax prf) _ = Lax prf
-
-wknSmallerR : (b1 : Bool) -> SmallerX b2 xs ys -> SmallerX (b1 || b2) xs ys
-wknSmallerR b1 (Strict prf) =
-  if b1 then ofSmaller prf else ofSmaller prf
-wknSmallerR b1 (Lax prf) =
-  if b1 then Lax prf else Lax prf
-
-forget : SmallerX b xs ys -> SmallerX True xs ys
-forget = wknSmallerR True
-
-toSmaller : {xs, ys : List a} -> (0 _ : SmallerX False xs ys) -> xs `Smaller` ys
-toSmaller {xs = []} {ys = []} (Strict prf) impossible
-toSmaller {xs = []} {ys = (y :: ys)} (Strict prf) = LTESucc LTEZero
-toSmaller {xs = (x :: xs)} {ys = []} (Strict prf) impossible
-toSmaller {xs = (x :: xs)} {ys = (y :: ys)} (Strict (LTESucc prf)) = LTESucc (toSmaller (Strict prf))
-
-anyCons : (b : Bool) -> (bs : List Bool) -> any Basics.id (b :: bs) = b || any Basics.id bs
-anyCons b [] = sym (orFalseNeutral b)
-anyCons b (b' :: bs) =
-  trans (anyCons (b || b') bs) $
-  trans (sym $ orAssociative b b' (any id bs))
-        (cong (b ||) (sym $ anyCons b' bs))
-
-anyTrue : (bs : List Bool) -> any Basics.id (True :: bs) = True
-anyTrue = anyCons True
-
--- Return Type
-
-namespace M
-  public export
-  data M : List a -> Bool -> Type -> Type where
-    Err : String -> M xs nil b
-    Ok : (res : b) -> (ys : List a) -> (0 prf : SmallerX nil ys xs) -> M xs nil b
-
-  export
-  Functor (M xs nil) where
-    map f (Err msg) = Err msg
-    map f (Ok res ys prf) = Ok (f res) ys prf
-
-  export
-  pure : {xs : List a} -> (x : b) -> M xs True b
-  pure x = Ok x xs (Lax reflexive)
-
-  export
-  (>>=) :
-    M xs nil b ->
-    (b -> {ys : List a} -> {auto 0 prf : SmallerX nil ys xs} -> M ys nil' c) ->
-    M xs (nil && nil') c
-  Err str >>= f = Err str
-  Ok res ys prf >>= f =
-    case f {ys, prf} res of
-      Err str => Err str
-      Ok res' zs prf' => Ok res' zs (rewrite andCommutative nil nil' in transX prf' prf)
-
-  export
-  take :
-    Eq a =>
-    Interpolation a =>
-    (toks : List a) ->
-    (xs : List (WithBounds (Token a))) ->
-    M xs False String
-  take [tok] [] = Err "expected \{tok}; got end of input"
-  take toks [] = Err "expected one of: \{join ", " $ map (\k => "\{k}") toks}; got end of input"
-  take toks (x :: xs) =
-    if x.val.kind `elem` toks
-    then Ok x.val.text xs (Strict reflexive)
-    else case toks of
-      [tok] => Err "\{x.bounds}: expected \{tok}; got \{x.val.kind}"
-      toks => Err "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") toks}; got \{x.val.kind}"
-
-  export
-  bounds : (xs : List (WithBounds a)) -> M xs True (Bool, Bounds)
-  bounds [] = Ok (True, MkBounds (-1) (-1) (-1) (-1)) [] (Lax reflexive)
-  bounds (x :: xs) = Ok (x.isIrrelevant, x.bounds) (x :: xs) (Lax reflexive)
-
-  export
-  wknL : M xs b1 a -> (b2 : Bool) -> M xs (b1 || b2) a
-  wknL (Err msg) b2 = Err msg
-  wknL (Ok res ys prf) b2 = Ok res ys (wknSmallerL prf b2)
-
-  export
-  wknR : (b1 : Bool) -> M xs b2 a -> M xs (b1 || b2) a
-  wknR b1 (Err msg) = Err msg
-  wknR b1 (Ok res ys prf) = Ok res ys (wknSmallerR b1 prf)
-
-  export
-  anyL :
-    (b : Bool) -> {0 bs : List Bool} ->
-    M xs (any Basics.id bs) a -> M xs (any Basics.id (b :: bs)) a
-  anyL b m = rewrite anyCons b bs in wknR b m
-
-  export
-  anyR : (bs : List Bool) -> M xs b a -> M xs (any Basics.id (b :: bs)) a
-  anyR bs m = rewrite anyCons b bs in wknL m (any id bs)
-
--- The Big Function
-
-||| Searches `sets` for the first occurence of `x`.
-||| On failure, returns the index for the nil element, if it exists.
-|||
-||| # Unsafe Invariants
-||| * `nils` has at most one `True` element
-||| * `sets` are disjoint
-lookahead :
-  Eq a =>
-  (x : Maybe a) ->
-  (nils : List Bool) ->
-  (sets : Lazy (All (const $ List a) nils)) ->
-  Maybe (Any (const ()) nils)
-lookahead x [] [] = Nothing
-lookahead x (nil :: nils) (set :: sets) =
-  (do
-    x <- x
-    if x `elem` set then Just (Here ()) else Nothing)
-  <|> There <$> lookahead x nils sets
-  <|> (if nil then Just (Here ()) else Nothing)
-
-parser :
-  (e : Eq i) => Interpolation i =>
-  (p : Parser i nil locked free a) ->
-  {penv1 : _} ->
-  {penv2 : _} ->
-  {0 fenv1 : _} ->
-  {0 fenv2 : _} ->
-  (0 wf : So (wellTyped e penv1 penv2 fenv1 fenv2 p)) ->
-  (xs : List (WithBounds (Token i))) ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free ->
-  M xs nil a
-parserChain :
-  (e : Eq i) => Interpolation i =>
-  (ps : ParserChain i nil locked free as) ->
-  {penv1 : _} ->
-  {penv2 : _} ->
-  {0 fenv1 : _} ->
-  {0 fenv2 : _} ->
-  (0 wf : So (wellTypedChain e penv1 penv2 fenv1 fenv2 ps)) ->
-  (xs : List (WithBounds (Token i))) ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free ->
-  M xs nil (HList as)
-parserOneOf :
-  (e : Eq i) => Interpolation i =>
-  {nils : List Bool} ->
-  (at : Any (const ()) nils) ->
-  (ps : All (\nil => Parser i nil locked free a) nils) ->
-  {penv1 : _} ->
-  {penv2 : _} ->
-  {0 fenv1 : _} ->
-  {0 fenv2 : _} ->
-  (0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)) ->
-  (xs : List (WithBounds (Token i))) ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked ->
-  All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free ->
-  M xs (any Basics.id nils) a
-
-parser (Var x) wf xs env1 env2 = (indexAll x.pos env2).value xs (Lax reflexive)
-parser (Lit text) wf xs env1 env2 = take [text] xs
-parser (Seq ps) wf xs env1 env2 =
-  parserChain ps wf xs env1 env2
-parser (OneOf {nils} ps) wf [] env1 env2 =
-  let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in
-  let sets = peekAll penv2 ps in
-  case lookahead Nothing nils sets of
-    Nothing => Err "unexpected end of input"
-    Just at => parserOneOf at ps (snd wfs) [] env1 env2
-parser (OneOf {nils} ps) wf (x :: xs) env1 env2 =
-  let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in
-  let sets = peekAll penv2 ps in
-  case lookahead (Just x.val.kind) nils sets of
-    Nothing => Err "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") $ concat $ forget sets}; got \{x.val.kind}"
-    Just at => parserOneOf at ps (snd wfs) (x :: xs) env1 env2
-parser (Fix {a, nil} x p) wf xs env1 env2 =
-  let f = parser p wf in
-  sizeInd {P = \ys => (0 prf : SmallerX True ys xs) -> M ys nil a}
-    (\ys, rec, lte =>
-      f ys
-        (  mapProperty (map (\f, zs, 0 prf => f zs $ transX prf lte)) env1
-        :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte)))
-        )
-        (mapProperty (map (\f, zs, prf => f zs $ transX prf lte)) env2))
-    xs (Lax reflexive)
-parser (Map f p) wf xs env1 env2 =
-  f <$> parser p wf xs env1 env2
-parser (WithBounds p) wf xs env1 env2 = do
-  (irrel, bounds) <- bounds xs
-  rewrite sym $ andTrueNeutral nil
-  x <- parser p wf _
-         (mapProperty (map (\f, zs, 0 prf => f zs $ transX {b2 = True} prf %search)) env1)
-         (mapProperty (map (\f, zs, 0 prf => f zs $ transX prf %search)) env2)
-  pure (MkBounded x irrel bounds)
-
-parserChain [] wf xs env1 env2 = Ok [] xs (Lax reflexive)
-parserChain ((::) {nil1 = False, nil2} p ps) wf xs env1 env2 =
-  let 0 wfs = soAnd wf in
-  let 0 wfs' = soAnd (snd wfs) in do
-    x <- parser p (fst wfs') xs env1 env2
-    y <- parserChain ps (snd wfs')
-          _
-          [<]
-          (  mapProperty (map (\f, zs, 0 prf => f zs $ forget $ transX {b2 = False} prf %search)) env2
-          ++ mapProperty (map (\f, zs, 0 prf => f zs $ transX prf %search)) env1
-          )
-    pure (x :: y)
-parserChain ((::) {nil1 = True, nil2} p ps) wf xs env1 env2 =
-  let 0 wfs = soAnd wf in
-  let 0 wfs' = soAnd (snd wfs) in do
-    x <- parser p (fst wfs') xs env1 env2
-    rewrite sym $ andTrueNeutral nil2
-    y <- parserChain ps (snd wfs')
-           _
-           (mapProperty (map (\f, zs, prf => f zs $ transX {b2 = True} prf %search)) env1)
-           (mapProperty (map (\f, zs, prf => f zs $ transX prf %search)) env2)
-    pure (x :: y)
-
-parserOneOf {nils = nil :: nils} (Here ()) (p :: ps) wf xs env1 env2 =
-  let 0 wfs = soAnd wf in
-  anyR nils (parser p (fst wfs) xs env1 env2)
-parserOneOf {nils = nil :: nils} (There at) (p :: ps) wf xs env1 env2 =
-  let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in
-  anyL nil (parserOneOf at ps (snd wfs) xs env1 env2)
-
-export
-parse :
-  (e : Eq i) => Interpolation i =>
-  (p : Parser i nil [<] [<] a) ->
-  {auto 0 wf : So (wellTyped e [<] [<] [<] [<] p)} ->
-  (xs : List (WithBounds (Token i))) -> M xs nil a
-parse p xs = parser p wf xs [<] [<]
-
--- Functor ---------------------------------------------------------------------
-
-public export
-(++) :
-  {nil2 : Bool} ->
-  ParserChain i nil1 locked free as ->
-  ParserChain i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) bs ->
-  ParserChain i (nil1 && nil2) locked free (as ++ bs)
-[] ++ qs = qs
-((::) {nil1 = False, nil2} p ps) ++ qs =
-  p ::
-  (  ps
-  ++ rewrite linUnlessLin (Bool, Type) nil2 in
-     rewrite linUnlessLin (Bool, Type) (not nil2) in
-     qs)
-((::) {nil1 = True, nil2} p ps) ++ qs = p :: (ps ++ qs)
-
-public export
-(<**>) :
-  {nil1, nil2 : Bool} ->
-  Parser i nil1 locked free a ->
-  Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b ->
-  Parser i (nil1 && nil2) locked free (a, b)
-p <**> Seq ps = Map (\(x :: xs) => (x, xs)) $ Seq (p :: ps)
--- HACK: andTrueNeutral isn't public, so do a full case split.
-(<**>) {nil1 = True, nil2 = True} p q = Map (\[x, y] => (x, y)) $ Seq [p, q]
-(<**>) {nil1 = True, nil2 = False} p q = Map (\[x, y] => (x, y)) $ Seq [p, q]
-(<**>) {nil1 = False, nil2 = True} p q = Map (\[x, y] => (x, y)) $ Seq [p, q]
-(<**>) {nil1 = False, nil2 = False} p q = Map (\[x, y] => (x, y)) $ Seq [p, q]
-
-public export
-Functor (Parser i nil locked free) where
-  map f (Map g p) = Map (f . g) p
-  map f p = Map f p
-
-public export
-Applicative (Parser i True locked free) where
-  pure x = map (const x) (Seq [])
-  p <*> q = map (\(f, x) => f x) (p <**> q)
-
--- Combinator ------------------------------------------------------------------
-
-public export
-(<|>) :
-  {nil1, nil2 : Bool} ->
-  Parser i nil1 locked free a ->
-  Parser i nil2 locked free a ->
-  {auto 0 prf : length (filter Basics.id [nil1, nil2]) `LTE` 1} ->
-  Parser i (nil1 || nil2) locked free a
-p <|> q = OneOf [p, q]
-
-public export
-(<||>) :
-  {nil1, nil2 : Bool} ->
-  Parser i nil1 locked free a ->
-  Parser i nil2 locked free b ->
-  {auto 0 prf : length (filter Basics.id [nil1, nil2]) `LTE` 1} ->
-  Parser i (nil1 || nil2) locked free (Either a b)
-p <||> q = Left <$> p <|> Right <$> q
-
-public export
-(**>) :
-  {nil1, nil2 : Bool} ->
-  Parser i nil1 locked free a ->
-  Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b ->
-  Parser i (nil1 && nil2) locked free b
-p **> q = snd <$> (p <**> q)
-
-public export
-(<**) :
-  {nil1, nil2 : Bool} ->
-  Parser i nil1 locked free a ->
-  Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b ->
-  Parser i (nil1 && nil2) locked free a
-p <** q = fst <$> (p <**> q)
-
-public export
-match : TokenKind i => (kind : i) -> Parser i False locked free (TokType kind)
-match kind = Map (tokValue kind) $ Lit kind
-
-public export
-enclose :
-  {b1, b2, b3 : Bool} ->
-  (left : Parser i b1 locked free ()) ->
-  (right :
-    Parser i b3
-      (linUnless b2 (linUnless b1 locked))
-      ((free ++ linUnless (not b1) locked) ++ linUnless (not b2) (linUnless b1 locked))
-      ()) ->
-  Parser i b2 (linUnless b1 locked) (free ++ linUnless (not b1) locked) a ->
-  Parser i (b1 && b2 && b3 && True) locked free a
-enclose left right p = (\[_, x, _] => x) <$> Seq {as = [(), a, ()]} [left, p, right]
-
-public export
-option : Parser i False locked free a -> Parser i True locked free (Maybe a)
-option p = (Just <$> p) <|> pure Nothing
-
-public export
-plus :
-  {auto len : LengthOf locked} ->
-  Parser i False locked free a ->
-  Parser i False locked free (List1 a)
-plus p =
-  Fix "plus"
-    (   uncurry (:::)
-    <$> (rename (Drop Id) Id p <**> maybe [] forget <$> option (Var $ %%% "plus")))
-
-public export
-star :
-  {auto len : LengthOf locked} ->
-  Parser i False locked free a ->
-  Parser i True locked free (List a)
-star p = maybe [] forget <$> option (plus p)
-
-public export
-sepBy1 :
-  {auto len : LengthOf locked} ->
-  (sep : Parser i False locked free ()) ->
-  Parser i False locked free a ->
-  Parser i False locked free (List1 a)
-sepBy1 sep p = uncurry (:::) <$> (p <**> star (weaken len sep **> weaken len p))
-
-public export
-sepBy :
-  {auto len : LengthOf locked} ->
-  (sep : Parser i False locked free ()) ->
-  Parser i False locked free a ->
-  Parser i True locked free (List a)
-sepBy sep p = maybe [] forget <$> option (sepBy1 sep p)
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 3c5d214..884256f 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -5,9 +5,9 @@ import public Inky.Type
 import Data.List.Quantifiers
 import Data.Singleton
 import Data.These
-import Inky.Data.SnocList.Quantifiers
-import Inky.Decidable
-import Inky.Decidable.Maybe
+import Flap.Data.SnocList.Quantifiers
+import Flap.Decidable
+import Flap.Decidable.Maybe
 
 %hide Prelude.Ops.infixl.(>=>)
 
@@ -85,13 +85,6 @@ data NotFunction : (bound : List String) -> (a : Ty tyCtx) -> Type
 %name NotFunction contra
 
 export
-isFunctionRecompute :
-  {a : Ty tyCtx} -> IsFunction bound a dom cod -> (Singleton dom, Singleton cod)
-isFunctionRecompute Done = (Val _, Val _)
-isFunctionRecompute (Step {a} prf) =
-  mapFst (\case Val _ => Val _) $ isFunctionRecompute prf
-
-export
 isFunctionUnique :
   IsFunction bound a dom cod -> IsFunction bound a dom' cod' -> (dom = dom', cod = cod')
 isFunctionUnique Done Done = (Refl, Refl)
diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr
index 6027d68..8de671c 100644
--- a/src/Inky/Term/Checks.idr
+++ b/src/Inky/Term/Checks.idr
@@ -5,49 +5,14 @@ import Data.DPair
 import Data.List.Quantifiers
 import Data.Singleton
 import Data.These
-import Inky.Data.SnocList.Quantifiers
-import Inky.Decidable
-import Inky.Decidable.Maybe
+import Flap.Data.SnocList.Quantifiers
+import Flap.Decidable
+import Flap.Decidable.Maybe
 import Inky.Term
+import Inky.Term.Recompute
 
 %hide Prelude.Ops.infixl.(>=>)
 
--- Can recompute type from synthesis proof
-
-export
-synthsRecompute :
-  {tyEnv : _} -> {tmEnv : _} -> {e : _} ->
-  Synths tyEnv tmEnv e a -> Singleton a
-checkSpineRecompute :
-  {tyEnv : _} -> {tmEnv : _} -> {a : _} ->
-  CheckSpine tyEnv tmEnv a ts b -> Singleton b
-allSynthsRecompute :
-  {tyEnv : _} -> {tmEnv : _} -> {es : Context _} ->
-  {0 as : Row (Ty [<])} ->
-  AllSynths tyEnv tmEnv es as -> Singleton as
-
-synthsRecompute (AnnotS wf prf) = Val _
-synthsRecompute VarS = Val _
-synthsRecompute (LetS prf1 prf2) with (synthsRecompute prf1)
-  _ | Val _ = synthsRecompute prf2
-synthsRecompute (LetTyS wf prf) = synthsRecompute prf
-synthsRecompute (AppS prf prfs) with (synthsRecompute prf)
-  _ | Val _ = checkSpineRecompute prfs
-synthsRecompute (TupS prfs) with (allSynthsRecompute prfs)
-  _ | Val _ = Val _
-synthsRecompute (PrjS prf i) with (synthsRecompute prf)
-  _ | Val _ = [| (nameOf i).value |]
-synthsRecompute (UnrollS prf) with (synthsRecompute prf)
-  _ | Val _ = Val _
-synthsRecompute (MapS f g h) = Val _
-
-checkSpineRecompute [] = Val _
-checkSpineRecompute (prf :: prfs) = checkSpineRecompute prfs
-
-allSynthsRecompute [<] = Val _
-allSynthsRecompute (prfs :< prf) with (allSynthsRecompute prfs) | (synthsRecompute prf)
-  _ | Val _ | Val _ = Val _
-
 -- Synthesis gives unique types
 
 synthsUnique : Synths tyEnv tmEnv e a -> Synths tyEnv tmEnv e b -> a = b
diff --git a/src/Inky/Term/Compile.idr b/src/Inky/Term/Compile.idr
new file mode 100644
index 0000000..0867cd2
--- /dev/null
+++ b/src/Inky/Term/Compile.idr
@@ -0,0 +1,316 @@
+module Inky.Term.Compile
+
+-- For DAll
+import public Inky.Type.Substitution
+
+import Data.Maybe
+import Data.List.Quantifiers
+import Data.Singleton
+import Flap.Decidable
+import Flap.Decidable.Maybe
+import Inky.Term
+import Inky.Term.Recompute
+import Text.PrettyPrint.Prettyprinter
+
+-- Utilities -------------------------------------------------------------------
+
+mkLet : (bind, val, body: Doc ann) -> Doc ann
+mkLet bind val body =
+  parens $ align $ hang 1 $
+    "let" <++> parens (group $ parens $ align $ bind <++> group val) <++>
+    group body
+
+mkAbs : (bind, body: Doc ann) -> Doc ann
+mkAbs bind body =
+  parens $ align $ hang 1 $
+    "lambda" <++> parens bind <++>
+    group body
+
+mkTup : Context (Doc ann) -> Doc ann
+mkTup parts =
+  let
+    f = \lx =>
+      group $ parens $ align $ hang 2 $
+        pretty lx.name <++> "." <++> "," <+> group lx.value
+  in
+  "`" <+> group (parens $ align $ concatWith (<++>) $ map f parts <>> [])
+
+mkPrj : Doc ann -> String -> Doc ann
+mkPrj x l =
+  parens $ align $
+    pretty "assq-ref" <++>
+    group x <++>
+    pretty "'" <+> pretty l
+
+mkInj : String -> Doc ann -> Doc ann
+mkInj l x =
+  parens $ align $
+    "cons" <++>
+    "'" <+> pretty l <++>
+    group x
+
+mkCase : Doc ann -> Context (Doc ann, Doc ann) -> Doc ann
+mkCase target branches =
+  let
+    f = \lxy =>
+      group $ parens $ align $
+        parens ("'" <+> pretty lxy.name <++> "." <++> fst lxy.value) <++>
+        group (snd lxy.value)
+  in
+  parens $ align $ hang 2 $
+    "match" <++>
+    group target <++>
+    concatWith (<++>) (map f branches <>> [])
+
+-- Create a "unique" name from a type ------------------------------------------
+
+hashType : Ty tyCtx -> String
+hashTypes : Context (Ty tyCtx) -> List String
+
+hashType (TVar i) = "V" ++ show i
+hashType (TArrow a b) = concat ["A", hashType a, hashType b]
+hashType (TProd (MkRow as _)) = concat ("P" :: hashTypes as)
+hashType (TSum (MkRow as _)) = concat ("S" :: hashTypes as)
+hashType (TFix x a) = concat ["F", hashType a]
+
+hashTypes [<] = ["N"]
+hashTypes (as :< (l :- a)) = ["L", l, hashType a] ++ hashTypes as
+
+-- Compile map and fold --------------------------------------------------------
+
+compileMap :
+  {a : Ty tyCtx} ->
+  (0 wf : WellFormed a) -> (i : Var tyCtx) ->
+  (0 prf : i `StrictlyPositiveIn` a) ->
+  (f, t : Doc ann) -> Doc ann
+eagerCompileMap :
+  {a : Ty tyCtx} ->
+  (0 wf : WellFormed a) -> (i : Var tyCtx) ->
+  (0 prf : i `StrictlyPositiveIn` a) ->
+  (f, t : Doc ann) -> Doc ann
+compileMapTuple :
+  {as : Context (Ty tyCtx)} ->
+  (0 wf : AllWellFormed as) -> (i : Var tyCtx) ->
+  (0 prfs : i `StrictlyPositiveInAll` as) ->
+  (f, t : Doc ann) -> All (Assoc0 $ Doc ann) as.names
+compileMapCase :
+  {as : Context (Ty tyCtx)} ->
+  (0 wf : AllWellFormed as) -> (i : Var tyCtx) ->
+  (0 prfs : i `StrictlyPositiveInAll` as) ->
+  (fun : Doc ann) -> All (Assoc0 $ (Doc ann, Doc ann)) as.names
+
+compileFold :
+  {a : Ty (tyCtx :< x)} ->
+  (0 wf : WellFormed a) ->
+  (0 prf : %% x `StrictlyPositiveIn` a) ->
+  (target, bind, body : Doc ann) -> Doc ann
+
+compileMap wf i prf f t =
+  if isJust (does $ strengthen i a)
+  then t
+  else eagerCompileMap wf i prf f t
+
+eagerCompileMap (TVar {i = j}) i TVar f t with (i `decEq` j)
+  _ | True `Because` _ = parens (f <++> t)
+  _ | False `Because` _ = t
+eagerCompileMap (TArrow _ _) i (TArrow prf) f t = t
+eagerCompileMap (TProd wfs) i (TProd prfs) f t =
+  mkTup $ fromAll $ compileMapTuple wfs i prfs f t
+eagerCompileMap (TSum wfs) i (TSum prfs) f t =
+  mkCase t $ fromAll $ compileMapCase wfs i prfs f
+eagerCompileMap (TFix sp wf) i (TFix prf) f t =
+  compileFold wf sp t (pretty "_eta") $
+  eagerCompileMap wf (ThereVar i) prf f (pretty "_eta")
+
+compileMapTuple [<] i [<] f t = [<]
+compileMapTuple ((:<) wfs {n} wf) i (prfs :< prf) f t =
+  compileMapTuple wfs i prfs f t :<
+  (n :- compileMap wf i prf f (mkPrj t n))
+
+compileMapCase [<] i [<] f = [<]
+compileMapCase ((:<) wfs {n} wf) i (prfs :< prf) f =
+  compileMapCase wfs i prfs f :<
+  (n :- (pretty "_eta", mkInj n (compileMap wf i prf f $ pretty "_eta")))
+
+compileFold {a} wf prf target bind body =
+  let name = pretty "fold-" <+> pretty (hashType a) in
+  let
+    fun = parens $ align $ hang 1 $
+      "define" <++> parens (name <++> name <+> "-arg") <++>
+      group (mkLet bind (compileMap wf (%% x) prf name (name <+> "-arg")) body)
+  in
+  parens $ align $ hang 1 $
+    "begin" <++>
+    group fun <++>
+    parens (name <++> target)
+
+-- Compile any term ------------------------------------------------------------
+
+export
+compileSynths :
+  {tmCtx : SnocList String} ->
+  {t : Term mode m tyCtx tmCtx} ->
+  {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+  {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+  (0 tyWf : DAll WellFormed tyEnv) ->
+  (0 tmWf : DAll WellFormed tmEnv) ->
+  (0 _ : Synths tyEnv tmEnv t a) ->
+  Doc ann
+export
+compileChecks :
+  {tmCtx : SnocList String} ->
+  {t : Term mode m tyCtx tmCtx} ->
+  {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+  {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+  (0 tyWf : DAll WellFormed tyEnv) ->
+  (0 tmWf : DAll WellFormed tmEnv) ->
+  {a : Ty [<]} ->
+  (0 wf : WellFormed a) ->
+  (0 _ : Checks tyEnv tmEnv a t) ->
+  Doc ann
+compileSpine :
+  {tmCtx : SnocList String} ->
+  {ts : List (Term mode m tyCtx tmCtx)} ->
+  {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+  {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+  (0 tyWf : DAll WellFormed tyEnv) ->
+  (0 tmWf : DAll WellFormed tmEnv) ->
+  {a : Ty [<]} ->
+  (0 wf : WellFormed a) ->
+  (0 _ : CheckSpine tyEnv tmEnv a ts b) ->
+  (fun : Doc ann) ->
+  Doc ann
+compileAllSynths :
+  {tmCtx : SnocList String} ->
+  {ts : Context (Term mode m tyCtx tmCtx)} ->
+  {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+  {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+  (0 tyWf : DAll WellFormed tyEnv) ->
+  (0 tmWf : DAll WellFormed tmEnv) ->
+  (0 _ : AllSynths tyEnv tmEnv ts as) ->
+  All (Assoc0 $ Doc ann) ts.names
+compileAllChecks :
+  {tmCtx : SnocList String} ->
+  {ts : Context (Term mode m tyCtx tmCtx)} ->
+  {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+  {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+  (0 tyWf : DAll WellFormed tyEnv) ->
+  (0 tmWf : DAll WellFormed tmEnv) ->
+  {as : Context (Ty [<])} ->
+  (0 fresh : AllFresh as.names) ->
+  (0 wfs : AllWellFormed as) ->
+  (0 _ : AllChecks tyEnv tmEnv as ts) ->
+  All (Assoc0 $ Doc ann) ts.names
+compileAllBranches :
+  {tmCtx : SnocList String} ->
+  {ts : Context (x ** Term mode m tyCtx (tmCtx :< x))} ->
+  {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+  {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+  (0 tyWf : DAll WellFormed tyEnv) ->
+  (0 tmWf : DAll WellFormed tmEnv) ->
+  {as : Context (Ty [<])} ->
+  {a : Ty [<]} ->
+  (0 fresh : AllFresh as.names) ->
+  (0 wfs : AllWellFormed as) ->
+  (0 wf : WellFormed a) ->
+  (0 _ : AllBranches tyEnv tmEnv as a ts) ->
+  All (Assoc0 (Doc ann, Doc ann)) ts.names
+
+compileSynths tyWf tmWf (AnnotS wf prf) = compileChecks tyWf tmWf (subWf tyWf wf) prf
+compileSynths tyWf tmWf (VarS {i}) = pretty (unVal $ nameOf i.pos)
+compileSynths tyWf tmWf (LetS {x} prf1 prf2) =
+  case synthsRecompute prf1 of
+    Val _ =>
+      mkLet (pretty x)
+        (compileSynths tyWf tmWf prf1)
+        (compileSynths tyWf (tmWf :< (x :- synthsWf tyWf tmWf prf1)) prf2)
+compileSynths tyWf tmWf (LetTyS {x} wf prf) =
+  compileSynths (tyWf :< (x :- subWf tyWf wf)) tmWf prf
+compileSynths tyWf tmWf (AppS prf prfs) =
+  case synthsRecompute prf of
+    Val _ => compileSpine tyWf tmWf (synthsWf tyWf tmWf prf) prfs (compileSynths tyWf tmWf prf)
+compileSynths tyWf tmWf (TupS prfs) = mkTup $ fromAll $ compileAllSynths tyWf tmWf prfs
+compileSynths tyWf tmWf (PrjS {l} prf i) = mkPrj (compileSynths tyWf tmWf prf) l
+compileSynths tyWf tmWf (UnrollS prf) = compileSynths tyWf tmWf prf
+compileSynths tyWf tmWf (MapS (TFix {x} sp wf1) wf2 wf3) =
+  mkAbs (pretty "_fun") $
+  mkAbs (pretty "_arg") $
+  compileMap wf1 (%% x) sp (pretty "_fun") (pretty "_arg")
+
+compileChecks tyWf tmWf wf (AnnotC prf1 prf2) = compileSynths tyWf tmWf prf1
+compileChecks tyWf tmWf wf (VarC prf1 prf2) = compileSynths tyWf tmWf prf1
+compileChecks tyWf tmWf wf (LetC {x} prf1 prf2) =
+  case synthsRecompute prf1 of
+    Val _ =>
+      mkLet (pretty x)
+        (compileSynths tyWf tmWf prf1)
+        (compileChecks tyWf (tmWf :< (x :- synthsWf tyWf tmWf prf1)) wf prf2)
+compileChecks tyWf tmWf wf (LetTyC wf' {x} prf) =
+  compileChecks (tyWf :< (x :- subWf tyWf wf')) tmWf wf prf
+compileChecks tyWf tmWf wf (AbsC {bound} prf1 prf2) =
+  case isFunctionRecompute prf1 of
+    (Val _, Val _) =>
+      let 0 wfs = isFunctionWf prf1 wf in
+      foldr
+        (mkAbs . pretty)
+        (compileChecks tyWf (tmWf <>< fst wfs) (snd wfs) prf2)
+        bound
+compileChecks tyWf tmWf wf (AppC prf1 prf2) = compileSynths tyWf tmWf prf1
+compileChecks tyWf tmWf (TProd {as = MkRow as fresh} wfs) (TupC prfs) =
+  mkTup $ fromAll $ compileAllChecks tyWf tmWf fresh wfs prfs
+compileChecks tyWf tmWf wf (PrjC prf1 prf2) = compileSynths tyWf tmWf prf1
+compileChecks tyWf tmWf (TSum wfs) (InjC {l, as} i prf) =
+  case lookupRecompute as i of
+    Val i => case nameOf i of
+      Val _ => mkInj l $ compileChecks tyWf tmWf (indexAllWellFormed wfs i) prf
+compileChecks tyWf tmWf wf (CaseC {as = MkRow as fresh} prf prfs) =
+  case synthsRecompute prf of
+    Val _ =>
+      let
+        0 wfs : AllWellFormed as
+        wfs = case synthsWf tyWf tmWf prf of TSum prfs => prfs
+      in
+      mkCase
+        (compileSynths tyWf tmWf prf)
+        (fromAll $ compileAllBranches tyWf tmWf fresh wfs wf prfs)
+compileChecks tyWf tmWf (TFix {x} sp wf) (RollC prf) =
+  compileChecks tyWf tmWf (subWf [<x :- TFix sp wf] wf) prf
+compileChecks tyWf tmWf wf (UnrollC prf1 prf2) = compileSynths tyWf tmWf prf1
+compileChecks tyWf tmWf wf (FoldC {x, a, y} prf1 prf2) =
+  case synthsRecompute prf1 of
+    Val (TFix x a) =>
+      let
+        0 spwf : (%% x `StrictlyPositiveIn` a, WellFormed a)
+        spwf = case synthsWf tyWf tmWf prf1 of TFix sp wf => (sp, wf)
+      in
+      compileFold (snd spwf) (fst spwf)
+        (compileSynths tyWf tmWf prf1)
+        (pretty y)
+        (compileChecks tyWf (tmWf :< (y :- (subWf [<x :- wf] $ snd spwf))) wf prf2)
+compileChecks tyWf tmWf wf (MapC prf1 prf2) = compileSynths tyWf tmWf prf1
+
+compileSpine tyWf tmWf wf [] fun = fun
+compileSpine tyWf tmWf (TArrow wf1 wf2) (prf :: prfs) fun =
+  let arg = compileChecks tyWf tmWf wf1 prf in
+  let fun = compileSpine tyWf tmWf wf2 prfs fun in
+  parens $ align $ hang 1 $ group fun <++> group arg
+
+compileAllSynths tyWf tmWf [<] = [<]
+compileAllSynths tyWf tmWf ((:<) prfs {l} prf) =
+  compileAllSynths tyWf tmWf prfs :< (l :- compileSynths tyWf tmWf prf)
+
+compileAllChecks tyWf tmWf fresh wfs Base = [<]
+compileAllChecks tyWf tmWf fresh wfs (Step {l, as} i prf prfs) =
+  case lookupRecompute (MkRow as fresh) i of
+    Val i => case nameOf i of
+      Val _ =>
+        compileAllChecks tyWf tmWf (dropElemFresh as fresh i) (dropAllWellFormed wfs i) prfs :<
+        (l :- compileChecks tyWf tmWf (indexAllWellFormed wfs i) prf)
+
+compileAllBranches tyWf tmWf fresh wfs wf Base = [<]
+compileAllBranches tyWf tmWf fresh wfs wf (Step {l, x, as} i prf prfs) =
+  case lookupRecompute (MkRow as fresh) i of
+    Val i => case nameOf i of
+      Val _ =>
+        compileAllBranches tyWf tmWf (dropElemFresh as fresh i) (dropAllWellFormed wfs i) wf prfs :<
+        (l :- (pretty x, compileChecks tyWf (tmWf :< (x :- indexAllWellFormed wfs i)) wf prf))
diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr
index 7051e4b..4bf8f05 100644
--- a/src/Inky/Term/Desugar.idr
+++ b/src/Inky/Term/Desugar.idr
@@ -2,8 +2,8 @@ module Inky.Term.Desugar
 
 import Data.List.Quantifiers
 import Data.Maybe
-import Inky.Data.List
-import Inky.Decidable
+import Flap.Data.List
+import Flap.Decidable
 import Inky.Term
 import Inky.Term.Substitution
 
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index 1c6eb58..4d68242 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -7,14 +7,15 @@ import Data.Nat
 import Data.List1
 import Data.String
 
-import Inky.Data.Context
-import Inky.Data.Context.Var
+import Flap.Data.Context
+import Flap.Data.Context.Var
+import Flap.Data.SnocList.Var
+import Flap.Data.SnocList.Thinning
+import Flap.Decidable
+import Flap.Decidable.Maybe
+import Flap.Parser
+
 import Inky.Data.Row
-import Inky.Data.SnocList.Var
-import Inky.Data.SnocList.Thinning
-import Inky.Decidable
-import Inky.Decidable.Maybe
-import Inky.Parser
 import Inky.Term
 import Inky.Type
 
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr
index bb19b2f..651d208 100644
--- a/src/Inky/Term/Pretty/Error.idr
+++ b/src/Inky/Term/Pretty/Error.idr
@@ -5,9 +5,10 @@ import Data.Singleton
 import Data.String
 import Data.These
 
-import Inky.Decidable.Maybe
+import Flap.Decidable.Maybe
+
 import Inky.Term
-import Inky.Term.Checks
+import Inky.Term.Recompute
 import Inky.Type.Pretty
 
 import Text.PrettyPrint.Prettyprinter
diff --git a/src/Inky/Term/Recompute.idr b/src/Inky/Term/Recompute.idr
new file mode 100644
index 0000000..dd0e809
--- /dev/null
+++ b/src/Inky/Term/Recompute.idr
@@ -0,0 +1,128 @@
+module Inky.Term.Recompute
+
+import Data.List.Quantifiers
+import Data.Singleton
+import Inky.Term
+import Inky.Type.Substitution
+
+%hide Prelude.Ops.infixl.(>=>)
+
+-- Can recompute arguments and result from function
+
+export
+isFunctionRecompute :
+  {bound : List String} -> {a : Ty tyCtx} ->
+  {0 dom : All (Assoc0 $ Ty tyCtx) bound} ->
+  (0 _ : IsFunction bound a dom cod) -> (Singleton dom, Singleton cod)
+isFunctionRecompute Done = (Val _, Val _)
+isFunctionRecompute (Step {a} prf) =
+  mapFst (\case Val _ => Val _) $ isFunctionRecompute prf
+
+-- Can recompute type from synthesis proof
+
+export
+synthsRecompute :
+  {tyEnv : _} -> {tmEnv : _} -> {e : _} ->
+  (0 _ : Synths tyEnv tmEnv e a) -> Singleton a
+checkSpineRecompute :
+  {tyEnv : _} -> {tmEnv : _} -> {a : _} -> {ts : _} ->
+  (0 _ : CheckSpine tyEnv tmEnv a ts b) ->
+  Singleton b
+allSynthsRecompute :
+  {tyEnv : _} -> {tmEnv : _} -> {es : Context _} ->
+  {0 as : Row (Ty [<])} ->
+  (0 _ : AllSynths tyEnv tmEnv es as) -> Singleton as
+
+synthsRecompute (AnnotS wf prf) = Val _
+synthsRecompute VarS = Val _
+synthsRecompute (LetS prf1 prf2) =
+  case synthsRecompute prf1 of
+    Val _ => synthsRecompute prf2
+synthsRecompute (LetTyS wf prf) = synthsRecompute prf
+synthsRecompute (AppS prf prfs) =
+  case synthsRecompute prf of
+    Val _ => checkSpineRecompute prfs
+synthsRecompute (TupS prfs) =
+  case allSynthsRecompute prfs of
+    Val _ => Val _
+synthsRecompute (PrjS {l, as} prf i) =
+  case synthsRecompute prf of
+    Val _ => case lookupRecompute as i of
+      Val i => [| (nameOf i).value |]
+synthsRecompute (UnrollS prf) =
+  case synthsRecompute prf of
+    Val _ => Val _
+synthsRecompute (MapS f g h) = Val _
+
+checkSpineRecompute [] = Val _
+checkSpineRecompute (prf :: prfs) = checkSpineRecompute prfs
+
+allSynthsRecompute [<] = Val _
+allSynthsRecompute (prfs :< prf) =
+  case (allSynthsRecompute prfs, synthsRecompute prf) of
+    (Val _, Val _) => Val _
+
+-- Synthesised types are well-formed
+
+export
+indexAllWellFormed : AllWellFormed as -> Elem (l :- a) as -> WellFormed a
+indexAllWellFormed (wfs :< wf) Here = wf
+indexAllWellFormed (wfs :< wf) (There i) = indexAllWellFormed wfs i
+
+export
+dropAllWellFormed : AllWellFormed as -> (i : Elem (l :- a) as) -> AllWellFormed (dropElem as i)
+dropAllWellFormed (wfs :< wf) Here = wfs
+dropAllWellFormed (wfs :< wf) (There i) = dropAllWellFormed wfs i :< wf
+
+export
+synthsWf :
+  {e : Term mode m tyCtx tmCtx} ->
+  {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+  {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+  DAll WellFormed tyEnv -> DAll WellFormed tmEnv ->
+  Synths tyEnv tmEnv e a -> WellFormed a
+checkSpineWf :
+  CheckSpine tyEnv tmEnv a ts b ->
+  WellFormed a -> WellFormed b
+allSynthsWf :
+  {es : Context (Term mode m tyCtx tmCtx)} ->
+  {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+  {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+  DAll WellFormed tyEnv -> DAll WellFormed tmEnv ->
+  AllSynths tyEnv tmEnv es as -> AllWellFormed as.context
+
+synthsWf tyWf tmWf (AnnotS wf prf) = subWf tyWf wf
+synthsWf tyWf tmWf (VarS {i}) = indexDAll i.pos tmWf
+synthsWf tyWf tmWf (LetS {x} prf1 prf2) =
+  case synthsRecompute prf1 of
+    Val _ => synthsWf tyWf (tmWf :< (x :- synthsWf tyWf tmWf prf1)) prf2
+synthsWf tyWf tmWf (LetTyS wf {x} prf) =
+  synthsWf (tyWf :< (x :- subWf tyWf wf)) tmWf prf
+synthsWf tyWf tmWf (AppS prf prfs) = checkSpineWf prfs (synthsWf tyWf tmWf prf)
+synthsWf tyWf tmWf (TupS prfs) = TProd (allSynthsWf tyWf tmWf prfs)
+synthsWf tyWf tmWf (PrjS prf i) =
+  let TProd wfs = synthsWf tyWf tmWf prf in
+  indexAllWellFormed wfs i
+synthsWf tyWf tmWf (UnrollS {x} prf) =
+  let TFix sp wf = synthsWf tyWf tmWf prf in
+  case synthsRecompute prf of
+    Val _ => subWf [<x :- TFix sp wf] wf
+synthsWf tyWf tmWf (MapS (TFix {x} sp wf1) wf2 wf3) =
+  let wf2 = subWf tyWf wf2 in
+  let wf3 = subWf tyWf wf3 in
+  TArrow (TArrow wf2 wf3) (TArrow
+    (subWf (tyWf :< (x :- wf2)) wf1)
+    (subWf (tyWf :< (x :- wf3)) wf1))
+
+checkSpineWf [] wf = wf
+checkSpineWf (prf :: prfs) (TArrow wf1 wf2) = checkSpineWf prfs wf2
+
+allSynthsWf tyWf tmWf [<] = [<]
+allSynthsWf tyWf tmWf (prfs :< prf) = allSynthsWf tyWf tmWf prfs :< synthsWf tyWf tmWf prf
+
+export
+isFunctionWf :
+  IsFunction bound a dom cod -> WellFormed a ->
+  (DAll WellFormed dom, WellFormed cod)
+isFunctionWf Done wf = ([], wf)
+isFunctionWf (Step {x} prf) (TArrow wf1 wf2) = mapFst ((x :- wf1) ::) $ isFunctionWf prf wf2
diff --git a/src/Inky/Term/Substitution.idr b/src/Inky/Term/Substitution.idr
index 690e38c..c99f5e6 100644
--- a/src/Inky/Term/Substitution.idr
+++ b/src/Inky/Term/Substitution.idr
@@ -1,7 +1,7 @@
 module Inky.Term.Substitution
 
 import Data.List.Quantifiers
-import Inky.Data.List
+import Flap.Data.List
 import Inky.Term
 
 public export
diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index 8c46328..5cd0b03 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -1,17 +1,17 @@
 module Inky.Type
 
-import public Inky.Data.Context.Var
+import public Flap.Data.Context.Var
+import public Flap.Data.SnocList.Var
 import public Inky.Data.Row
-import public Inky.Data.SnocList.Var
 import public Inky.Data.Thinned
 
 import Control.Function
 import Data.DPair
 import Data.These
 
-import Inky.Data.SnocList.Thinning
-import Inky.Decidable
-import Inky.Decidable.Maybe
+import Flap.Data.SnocList.Thinning
+import Flap.Decidable
+import Flap.Decidable.Maybe
 
 %hide Prelude.Ops.infixl.(>=>)
 
@@ -191,11 +191,29 @@ thinId (TFix x a) = cong (TFix x) (trans (thinCong (KeepId IdId) a) (thinId a))
 thinIdAll [<] = Refl
 thinIdAll (as :< (n :- a)) = cong2 (:<) (thinIdAll as) (cong (n :-) $ thinId a)
 
-export
+thinHomo :
+  (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (a : Ty ctx1) ->
+  thin f (thin g a) = thin (f . g) a
+thinHomoAll :
+  (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (as : Context (Ty ctx1)) ->
+  thinAll f (thinAll g as) = thinAll (f . g) as
+
+thinHomo f g (TVar i) = cong (TVar . toVar) $ sym $ indexPosComp f g i.pos
+thinHomo f g (TArrow a b) = cong2 TArrow (thinHomo f g a) (thinHomo f g b)
+thinHomo f g (TProd (MkRow as fresh)) = cong TProd $ rowCong $ thinHomoAll f g as
+thinHomo f g (TSum (MkRow as fresh)) = cong TSum $ rowCong $ thinHomoAll f g as
+thinHomo f g (TFix x a) = cong (TFix x) $ thinHomo (Keep f) (Keep g) a
+
+thinHomoAll f g [<] = Refl
+thinHomoAll f g (as :< (n :- a)) =
+  cong2 (:<) (thinHomoAll f g as) (cong (n :-) $ thinHomo f g a)
+
+public export
 Rename String Ty where
   rename = thin
   renameCong = thinCong
   renameId = thinId
+  renameHomo = thinHomo
 
 -- Alpha Equivalence ------------------------------------------------------------
 
@@ -521,14 +539,13 @@ namespace Strengthen
   data Strengthen : (i : Var ctx) -> Ty ctx -> Ty (dropElem ctx i.pos) -> Type
   public export
   data StrengthenAll :
-    (i : Var ctx) -> (as : Context (Ty ctx)) ->
-    All (Assoc0 $ Ty $ dropElem ctx i.pos) as.names -> Type
+    (i : Var ctx) -> Context (Ty ctx) -> Context (Ty $ dropElem ctx i.pos) -> Type
 
   data Strengthen where
     TVar : (j = index (dropPos i.pos) k) -> Strengthen i (TVar j) (TVar k)
     TArrow : Strengthen i a c -> Strengthen i b d -> Strengthen i (TArrow a b) (TArrow c d)
-    TProd : StrengthenAll i as.context bs -> Strengthen i (TProd as) (TProd $ fromAll bs as.fresh)
-    TSum : StrengthenAll i as.context bs -> Strengthen i (TSum as) (TSum $ fromAll bs as.fresh)
+    TProd : StrengthenAll i as.context bs.context -> Strengthen i (TProd as) (TProd bs)
+    TSum : StrengthenAll i as.context bs.context -> Strengthen i (TSum as) (TSum bs)
     TFix : Strengthen (ThereVar i) a b -> Strengthen i (TFix x a) (TFix x b)
 
   data StrengthenAll where
@@ -538,13 +555,20 @@ namespace Strengthen
   %name Strengthen prf
   %name StrengthenAll prfs
 
+export
+strengthenAllNames : StrengthenAll i as bs -> bs.names = as.names
+strengthenAllNames [<] = Refl
+strengthenAllNames ((:<) prfs {l} prf) = cong (:< l) (strengthenAllNames prfs)
+
 strengthenEq : Strengthen i a b -> a = thin (dropPos i.pos) b
-strengthenAllEq : StrengthenAll i as bs -> as = thinAll (dropPos i.pos) (fromAll bs)
+strengthenAllEq : StrengthenAll i as bs -> as = thinAll (dropPos i.pos) bs
 
 strengthenEq (TVar prf) = cong TVar prf
 strengthenEq (TArrow prf1 prf2) = cong2 TArrow (strengthenEq prf1) (strengthenEq prf2)
-strengthenEq (TProd {as = MkRow _ _} prfs) = cong TProd $ rowCong $ strengthenAllEq prfs
-strengthenEq (TSum {as = MkRow _ _} prfs) = cong TSum $ rowCong $ strengthenAllEq prfs
+strengthenEq (TProd {as = MkRow _ _, bs = MkRow _ _} prfs) =
+  cong TProd $ rowCong $ strengthenAllEq prfs
+strengthenEq (TSum {as = MkRow _ _, bs = MkRow _ _} prfs) =
+  cong TSum $ rowCong $ strengthenAllEq prfs
 strengthenEq (TFix prf) = cong (TFix _) $ strengthenEq prf
 
 strengthenAllEq [<] = Refl
@@ -583,8 +607,8 @@ strengthenSplit (TVar Refl) (TVar {i = %% n} contra) = void $ lemma _ _ contra
   lemma :
     (i : Elem x sx) -> (j : Elem y (dropElem sx i)) ->
     Not (toVar i = toVar (indexPos (dropPos i) j))
-  lemma Here j prf = absurd (toVarInjective prf)
-  lemma (There i) Here prf = absurd (toVarInjective prf)
+  lemma Here j prf = absurd @{HereThere} (toVarInjective prf)
+  lemma (There i) Here prf = absurd @{ThereHere} (toVarInjective prf)
   lemma (There i) (There j) prf = lemma i j $ toVarCong $ thereInjective $ toVarInjective prf
 strengthenSplit (TArrow prf1 prf2) (TArrow contras) =
   these (strengthenSplit prf1) (strengthenSplit prf2) (const $ strengthenSplit prf2) contras
@@ -602,7 +626,9 @@ strengthen :
 export
 strengthenAll :
   (i : Var ctx) -> (as : Context (Ty ctx)) ->
-  Proof (All (Assoc0 $ Ty $ dropElem ctx i.pos) as.names) (StrengthenAll i as) (i `OccursInAny` as)
+  Proof (Subset (Context (Ty $ dropElem ctx i.pos)) (\bs => bs.names = as.names))
+    (StrengthenAll i as . Subset.fst)
+    (i `OccursInAny` as)
 
 strengthen ((%%) x {pos = i}) (TVar ((%%) y {pos = j})) =
   map (TVar . toVar)
@@ -613,18 +639,21 @@ strengthen i (TArrow a b) =
   map (uncurry TArrow) (\(c, d) => uncurry TArrow) TArrow $
   all (strengthen i a) (strengthen i b)
 strengthen i (TProd (MkRow as fresh)) =
-  map (\bs => TProd $ fromAll bs fresh) (\_ => TProd) TProd $
+  map (\bs => TProd $ MkRow (fst bs) (rewrite snd bs in fresh)) (\_ => TProd) TProd $
   strengthenAll i as
 strengthen i (TSum (MkRow as fresh)) =
-  map (\bs => TSum $ fromAll bs fresh) (\_ => TSum) TSum $
+  map (\bs => TSum $ MkRow (fst bs) (rewrite snd bs in fresh)) (\_ => TSum) TSum $
   strengthenAll i as
 strengthen i (TFix x a) =
   map (TFix x) (\_ => TFix) TFix $
   strengthen (ThereVar i) a
 
-strengthenAll i [<] = Just [<] `Because` [<]
+strengthenAll i [<] = Just (Element [<] Refl) `Because` [<]
 strengthenAll i (as :< (l :- a)) =
-  map (\x => snd x :< (l :- fst x)) (\(_, _) => uncurry (:<) . swap) (And . swap) $
+  map
+    (\x => Element (fst (snd x) :< (l :- fst x)) (cong (:< l) (snd $ snd x)))
+    (\(_, _) => uncurry (:<) . swap)
+    (And . swap) $
   all (strengthen i a) (strengthenAll i as)
 
 -- Not Strictly Positive -----------------------------------------------------------
@@ -679,6 +708,20 @@ Uninhabited (i `NotPositiveInAny` [<]) where
   uninhabited (And contras) impossible
 
 export
+strongIsStrictlyPositive : Strengthen i a b -> i `StrictlyPositiveIn` a
+allStrongIsAllStrictlyPositive : StrengthenAll i as bs -> i `StrictlyPositiveInAll` as
+
+strongIsStrictlyPositive (TVar prf) = TVar
+strongIsStrictlyPositive (TArrow prf1 prf2) = TArrow (TArrow prf1 prf2)
+strongIsStrictlyPositive (TProd prfs) = TProd (allStrongIsAllStrictlyPositive prfs)
+strongIsStrictlyPositive (TSum prfs) = TSum (allStrongIsAllStrictlyPositive prfs)
+strongIsStrictlyPositive (TFix prf) = TFix (strongIsStrictlyPositive prf)
+
+allStrongIsAllStrictlyPositive [<] = [<]
+allStrongIsAllStrictlyPositive (prfs :< prf) =
+  allStrongIsAllStrictlyPositive prfs :< strongIsStrictlyPositive prf
+
+export
 strictlyPositiveSplit : i `StrictlyPositiveIn` a -> i `NotPositiveIn` a -> Void
 strictlyPositiveAllSplit : i `StrictlyPositiveInAll` as -> i `NotPositiveInAny` as -> Void
 
@@ -806,8 +849,8 @@ subAll : All (Assoc0 $ Thinned Ty ctx2) ctx1 -> Context (Ty ctx1) -> Context (Ty
 public export
 subAllNames :
   (f : All (Assoc0 $ Thinned Ty ctx2) ctx1) ->
-  (ctx : Context (Ty ctx1)) ->
-  (subAll f ctx).names = ctx.names
+  (env : Context (Ty ctx1)) ->
+  (subAll f env).names = env.names
 
 sub' env (TVar i) = (indexAll i.pos env).value.extract
 sub' env (TArrow a b) = TArrow (sub' env a) (sub' env b)
diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index 2785b87..91b28ba 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -1,7 +1,7 @@
 module Inky.Type.Pretty
 
 import Data.Singleton
-import Inky.Decidable
+import Flap.Decidable
 import Inky.Type
 import Text.PrettyPrint.Prettyprinter
 
diff --git a/src/Inky/Type/Substitution.idr b/src/Inky/Type/Substitution.idr
new file mode 100644
index 0000000..2a25d07
--- /dev/null
+++ b/src/Inky/Type/Substitution.idr
@@ -0,0 +1,364 @@
+module Inky.Type.Substitution
+
+import Data.List.Quantifiers
+import Flap.Decidable.Maybe
+import Inky.Type
+
+namespace SnocList
+  public export
+  data DAll : {0 ctx : SnocList String} -> (p : a -> Type) -> All (Assoc0 a) ctx -> Type where
+    Lin : DAll p [<]
+    (:<) : DAll p env -> Assoc0 p (n :- a) -> DAll p (env :< (n :- a))
+
+  %name DAll penv
+
+  export
+  indexDAll :
+    {0 p : a -> Type} ->
+    (i : Elem x ctx) -> {0 env : All (Assoc0 a) ctx} ->
+    DAll p env -> p (indexAll i env).value
+  indexDAll Here (penv :< (l :- px)) = px
+  indexDAll (There i) (penv :< (l :- px)) = indexDAll i penv
+
+  export
+  mapDProperty :
+    {0 p : a -> Type} ->
+    {0 q : b -> Type} ->
+    {0 f : a -> b} ->
+    (forall x. p x -> q (f x)) ->
+    DAll p env -> DAll q (mapProperty (map f) env)
+  mapDProperty g [<] = [<]
+  mapDProperty g (penv :< (l :- px)) = mapDProperty g penv :< (l :- g px)
+
+namespace List
+  public export
+  data DAll : {0 ctx : List String} -> (p : a -> Type) -> All (Assoc0 a) ctx -> Type where
+    Nil : DAll p []
+    (::) : Assoc0 p (n :- a) -> List.DAll p env -> DAll p ((n :- a) :: env)
+
+  %name List.DAll penv
+
+export
+(<><) : DAll p env1 -> List.DAll p env2 -> DAll p (env1 <>< env2)
+penv1 <>< [] = penv1
+penv1 <>< (px :: penv2) = (penv1 :< px) <>< penv2
+
+indexAllMap :
+  {0 p, q : a -> Type} ->
+  (0 f : forall x. p x -> q x) ->
+  (i : Elem x sx) -> (env : All p sx) ->
+  indexAll i (mapProperty f env) = f (indexAll i env)
+indexAllMap f Here (env :< px) = Refl
+indexAllMap f (There i) (env :< px) = indexAllMap f i env
+
+-- Strengthening ---------------------------------------------------------------
+
+skipsStrengthens :
+  {f : ctx1 `Thins` ctx2} ->
+  f `Skips` i.pos ->
+  (a : Ty ctx1) ->
+  (b ** Strengthen i (thin f a) b)
+skipsStrengthensAll :
+  {f : ctx1 `Thins` ctx2} ->
+  f `Skips` i.pos ->
+  (as : Context (Ty ctx1)) ->
+  (bs ** (StrengthenAll i (thinAll f as) bs, bs.names = as.names))
+
+skipsStrengthens skips (TVar j) =
+  let (k ** eq) = strong f skips j.pos in
+  (TVar k ** TVar eq)
+  where
+  strong :
+    forall ctx1, ctx2.
+    (f : ctx1 `Thins` ctx2) -> {0 i : Elem y ctx2} ->
+    f `Skips` i -> (j : Elem x ctx1) -> (k ** toVar (indexPos f j) = index (dropPos i) k)
+  strong (Drop {sx, sy} f) Here j = (toVar (indexPos f j) ** Refl)
+  strong (Drop f) (Also skips) j =
+    let (k ** eq) = strong f skips j in
+    (ThereVar k ** cong ThereVar eq)
+  strong (Keep f) (There skips) Here = (toVar Here ** Refl)
+  strong (Keep f) (There skips) (There j) =
+    let (k ** eq) = strong f skips j in
+    (ThereVar k ** cong ThereVar eq)
+skipsStrengthens skips (TArrow a b) =
+  let (a ** prf1) = skipsStrengthens skips a in
+  let (b ** prf2) = skipsStrengthens skips b in
+  (TArrow a b ** TArrow prf1 prf2)
+skipsStrengthens skips (TProd (MkRow as fresh)) =
+  let (as ** (prfs, eq)) = skipsStrengthensAll skips as in
+  (TProd (MkRow as (rewrite eq in fresh)) ** TProd prfs)
+skipsStrengthens skips (TSum (MkRow as fresh)) =
+  let (as ** (prfs, eq)) = skipsStrengthensAll skips as in
+  (TSum (MkRow as (rewrite eq in fresh)) ** TSum prfs)
+skipsStrengthens skips (TFix x a) =
+  let (a ** prf) = skipsStrengthens (There skips) a in
+  (TFix x a ** TFix prf)
+
+skipsStrengthensAll skips [<] = ([<] ** ([<], Refl))
+skipsStrengthensAll skips (as :< (l :- a)) =
+  let (bs ** (prfs, eq)) = skipsStrengthensAll skips as in
+  let (b ** prf) = skipsStrengthens skips a in
+  (bs :< (l :- b) ** (prfs :< prf, cong (:< l) eq))
+
+thinStrengthen :
+  (0 f : ctx1 `Thins` ctx2) ->
+  Strengthen i a b -> Strengthen (index f i) (thin f a) (thin (punchOut f i.pos) b)
+thinAllStrengthen :
+  (0 f : ctx1 `Thins` ctx2) ->
+  StrengthenAll i as bs -> StrengthenAll (index f i) (thinAll f as) (thinAll (punchOut f i.pos) bs)
+
+thinStrengthen f (TVar {j, k} prf) =
+  TVar $
+  rewrite sym $ indexPosComp (dropPos (indexPos f i.pos)) (punchOut f i.pos) k.pos in
+  rewrite (punchOutHomo f i.pos).indexPos k.pos in
+  rewrite indexPosComp f (dropPos i.pos) k.pos in
+  cong (index f) prf
+thinStrengthen f (TArrow prf1 prf2) = TArrow (thinStrengthen f prf1) (thinStrengthen f prf2)
+thinStrengthen f (TProd {as = MkRow _ _, bs = MkRow _ _} prfs) = TProd (thinAllStrengthen f prfs)
+thinStrengthen f (TSum {as = MkRow _ _, bs = MkRow _ _} prfs) = TSum (thinAllStrengthen f prfs)
+thinStrengthen f (TFix prf) = TFix (thinStrengthen (Keep f) prf)
+
+thinAllStrengthen f [<] = [<]
+thinAllStrengthen f (prfs :< prf) = thinAllStrengthen f prfs :< thinStrengthen f prf
+
+sub'Strengthen :
+  {a : Ty ctx1} ->
+  {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} ->
+  ((k : Var ctx1) ->
+    Proof (Ty (dropElem ctx2 j.pos))
+      (Strengthen j (indexAll k.pos env).value.extract)
+      (i = k)) ->
+  Strengthen i a b ->
+  (c ** Strengthen j (sub' env a) c)
+subAllStrengthen :
+  {as : Context (Ty ctx1)} ->
+  {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} ->
+  ((k : Var ctx1) ->
+    Proof (Ty (dropElem ctx2 j.pos))
+      (Strengthen j (indexAll k.pos env).value.extract)
+      (i = k)) ->
+  StrengthenAll i as bs ->
+  (cs ** (StrengthenAll j (subAll env as) cs, cs.names = as.names))
+
+sub'Strengthen envStr (TVar {j = k1, k = k2} eq) =
+  case envStr k1 of
+    Just b `Because` prf => (b ** prf)
+    Nothing `Because` prf =>
+      void $
+      skipsSplit (dropPosSkips i.pos) k2.pos $
+      replace {p = (\x => i.pos ~=~ x.pos)}
+        (trans prf eq)
+        Refl
+sub'Strengthen envStr (TArrow prf1 prf2) =
+  let (a ** prf1) = sub'Strengthen envStr prf1 in
+  let (b ** prf2) = sub'Strengthen envStr prf2 in
+  (TArrow a b ** TArrow prf1 prf2)
+sub'Strengthen envStr (TProd {as = MkRow as fresh} prfs) =
+  let (as ** (prfs, eq)) = subAllStrengthen envStr prfs in
+  (TProd (MkRow as (rewrite eq in fresh)) ** TProd prfs)
+sub'Strengthen envStr (TSum {as = MkRow as fresh} prfs) =
+  let (as ** (prfs, eq)) = subAllStrengthen envStr prfs in
+  (TSum (MkRow as (rewrite eq in fresh)) ** TSum prfs)
+sub'Strengthen envStr (TFix {x} prf) =
+  let (a ** prf) = sub'Strengthen envStr' prf in
+  (TFix x a ** TFix prf)
+  where
+  Env0 : All (Assoc0 $ Thinned Ty (ctx2 :< x)) ctx1
+  Env0 = mapProperty (map $ rename $ Drop Id) env
+
+  getEnv0 : (i : Elem y ctx1) -> indexAll i Env0 = map (rename $ Drop Id) (indexAll i env)
+  getEnv0 i = indexAllMap (map $ rename $ Drop Id) i env
+
+  Env' : All (Assoc0 $ Thinned Ty (ctx2 :< x)) (ctx1 :< x)
+  Env' = Env0 :< (x :- (TVar (%% x) `Over` Id))
+
+  getEnv' : Var (ctx1 :< x) -> Ty (ctx2 :< x)
+  getEnv' i = (indexAll i.pos Env').value.extract
+
+  envStr' :
+    (k : Var (ctx1 :< x)) ->
+    Proof (Ty (dropElem ctx2 j.pos :< x))
+      (Strengthen (ThereVar j) (getEnv' k))
+      (ThereVar i = k)
+  envStr' ((%%) _ {pos = Here}) = Just (TVar (%% x)) `Because` TVar Refl
+  envStr' ((%%) name {pos = There k}) =
+    map (thin $ Drop Id)
+      (\b, prf =>
+        rewrite getEnv0 k in
+        rewrite sym $ extractHomo (Drop {x} Id) (indexAll k env).value in
+        thinStrengthen (Drop Id) prf)
+      (\eq => cong ThereVar eq) $
+    envStr (%% name)
+
+subAllStrengthen envStr [<] = ([<] ** ([<], Refl))
+subAllStrengthen envStr ((:<) prfs {l} prf) =
+  let (cs ** (prfs, eq)) = subAllStrengthen envStr prfs in
+  let (c ** prf) = sub'Strengthen envStr prf in
+  (cs :< (l :- c) ** (prfs :< prf, cong (:< l) eq))
+
+-- Strict Positivity -----------------------------------------------------------
+
+thinStrictlyPositive :
+  (0 f : ctx1 `Thins` ctx2) ->
+  i `StrictlyPositiveIn` a ->
+  index f i `StrictlyPositiveIn` thin f a
+thinAllStrictlyPositive :
+  (0 f : ctx1 `Thins` ctx2) ->
+  i `StrictlyPositiveInAll` as ->
+  index f i `StrictlyPositiveInAll` thinAll f as
+
+thinStrictlyPositive f TVar = TVar
+thinStrictlyPositive f (TArrow prf) = TArrow (thinStrengthen f prf)
+thinStrictlyPositive f (TProd {as = MkRow _ _} prfs) = TProd (thinAllStrictlyPositive f prfs)
+thinStrictlyPositive f (TSum {as = MkRow _ _} prfs) = TSum (thinAllStrictlyPositive f prfs)
+thinStrictlyPositive f (TFix prf) = TFix (thinStrictlyPositive (Keep f) prf)
+
+thinAllStrictlyPositive f [<] = [<]
+thinAllStrictlyPositive f (prfs :< prf) =
+  thinAllStrictlyPositive f prfs :< thinStrictlyPositive f prf
+
+sub'StrictlyPositive :
+  {a : Ty ctx1} ->
+  {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} ->
+  ((k : Var ctx1) ->
+    Proof (Ty (dropElem ctx2 j.pos))
+      (Strengthen j (indexAll k.pos env).value.extract)
+      (i = k, j `StrictlyPositiveIn` (indexAll k.pos env).value.extract)) ->
+  i `StrictlyPositiveIn` a ->
+  j `StrictlyPositiveIn` sub' env a
+subAllStrictlyPositive :
+  {as : Context (Ty ctx1)} ->
+  {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} ->
+  ((k : Var ctx1) ->
+    Proof (Ty (dropElem ctx2 j.pos))
+      (Strengthen j (indexAll k.pos env).value.extract)
+      (i = k, j `StrictlyPositiveIn` (indexAll k.pos env).value.extract)) ->
+  i `StrictlyPositiveInAll` as ->
+  j `StrictlyPositiveInAll` subAll env as
+
+sub'StrictlyPositive envSp (TVar {j = k}) =
+  case envSp k of
+    Just a `Because` prf => strongIsStrictlyPositive prf
+    Nothing `Because` (Refl, prf) => prf
+sub'StrictlyPositive envSp (TArrow (TArrow prf1 prf2)) =
+  let envStr = \k => map id (\_ => id) fst $ envSp k in
+  let (_ ** str1) = sub'Strengthen envStr prf1 in
+  let (_ ** str2) = sub'Strengthen envStr prf2 in
+  TArrow (TArrow str1 str2)
+sub'StrictlyPositive envSp (TProd {as = MkRow _ _} prfs) = TProd (subAllStrictlyPositive envSp prfs)
+sub'StrictlyPositive envSp (TSum {as = MkRow _ _} prfs) = TSum (subAllStrictlyPositive envSp prfs)
+sub'StrictlyPositive envSp (TFix {x} prf) =
+  TFix (sub'StrictlyPositive envSp' prf)
+  where
+  Env0 : All (Assoc0 $ Thinned Ty (ctx2 :< x)) ctx1
+  Env0 = mapProperty (map $ rename $ Drop Id) env
+
+  getEnv0 : (i : Elem y ctx1) -> indexAll i Env0 = map (rename $ Drop Id) (indexAll i env)
+  getEnv0 i = indexAllMap (map $ rename $ Drop Id) i env
+
+  Env' : All (Assoc0 $ Thinned Ty (ctx2 :< x)) (ctx1 :< x)
+  Env' = Env0 :< (x :- (TVar (%% x) `Over` Id))
+
+  getEnv' : Var (ctx1 :< x) -> Ty (ctx2 :< x)
+  getEnv' i = (indexAll i.pos Env').value.extract
+
+  envSp' :
+    (k : Var (ctx1 :< x)) ->
+    Proof (Ty (dropElem ctx2 j.pos :< x))
+      (Strengthen (ThereVar j) (getEnv' k))
+      (ThereVar i = k, ThereVar j `StrictlyPositiveIn` (getEnv' k))
+  envSp' ((%%) _ {pos = Here}) = Just (TVar (%% x)) `Because` TVar Refl
+  envSp' ((%%) name {pos = There k}) =
+    map (thin $ Drop Id)
+      (\b, prf =>
+        rewrite getEnv0 k in
+        rewrite sym $ extractHomo (Drop {x} Id) (indexAll k env).value in
+        thinStrengthen (Drop Id) prf)
+      (\(eq, prf) =>
+        ( cong ThereVar eq
+        , rewrite getEnv0 k in
+          rewrite sym $ extractHomo (Drop {x} Id) (indexAll k env).value in
+          thinStrictlyPositive (Drop Id) prf
+        )) $
+    envSp (%% name)
+
+subAllStrictlyPositive envSp [<] = [<]
+subAllStrictlyPositive envSp (prfs :< prf) =
+  subAllStrictlyPositive envSp prfs :< sub'StrictlyPositive envSp prf
+
+-- Well Formedness -------------------------------------------------------------
+
+thinWf : (0 f : ctx1 `Thins` ctx2) -> WellFormed a -> WellFormed (thin f a)
+thinAllWf : (0 f : ctx1 `Thins` ctx2) -> AllWellFormed as -> AllWellFormed (thinAll f as)
+
+thinWf f TVar = TVar
+thinWf f (TArrow wf1 wf2) = TArrow (thinWf f wf1) (thinWf f wf2)
+thinWf f (TProd {as = MkRow _ _} wfs) = TProd (thinAllWf f wfs)
+thinWf f (TSum {as = MkRow _ _} wfs) = TSum (thinAllWf f wfs)
+thinWf f (TFix prf wf) = TFix (thinStrictlyPositive (Keep f) prf) (thinWf (Keep f) wf)
+
+thinAllWf f [<] = [<]
+thinAllWf f (wfs :< wf) = thinAllWf f wfs :< thinWf f wf
+
+sub'Wf :
+  {a : Ty ctx1} ->
+  {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} ->
+  DAll (\ty => WellFormed ty.value) env ->
+  WellFormed a ->
+  WellFormed (sub' env a)
+subAllWf :
+  {as : Context (Ty ctx1)} ->
+  {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} ->
+  DAll (\ty => WellFormed ty.value) env ->
+  AllWellFormed as ->
+  AllWellFormed (subAll env as)
+
+sub'Wf envWf (TVar {i}) =
+  thinWf (indexAll i.pos env).value.thins (indexDAll i.pos envWf)
+sub'Wf envWf (TArrow wf1 wf2) = TArrow (sub'Wf envWf wf1) (sub'Wf envWf wf2)
+sub'Wf envWf (TProd {as = MkRow _ _} wfs) = TProd (subAllWf envWf wfs)
+sub'Wf envWf (TSum {as = MkRow _ _} wfs) = TSum (subAllWf envWf wfs)
+sub'Wf envWf (TFix {x} prf wf) =
+  TFix
+    (sub'StrictlyPositive envSp prf)
+    (sub'Wf (mapDProperty {f = rename (Drop Id)} id envWf :< (x :- TVar)) wf)
+  where
+  Env0 : All (Assoc0 $ Thinned Ty (ctx2 :< x)) ctx1
+  Env0 = mapProperty (map $ rename $ Drop Id) env
+
+  getEnv0 : (i : Elem y ctx1) -> indexAll i Env0 = map (rename $ Drop Id) (indexAll i env)
+  getEnv0 i = indexAllMap (map $ rename $ Drop Id) i env
+
+  Env' : All (Assoc0 $ Thinned Ty (ctx2 :< x)) (ctx1 :< x)
+  Env' = Env0 :< (x :- (TVar (%% x) `Over` Id))
+
+  getEnv' : Var (ctx1 :< x) -> Ty (ctx2 :< x)
+  getEnv' i = (indexAll i.pos Env').value.extract
+
+  envSp :
+    (k : Var (ctx1 :< x)) ->
+    Proof (Ty ctx2)
+      (Strengthen (%% x) (getEnv' k))
+      ((%% x) = k, (%% x) `StrictlyPositiveIn` (getEnv' k))
+  envSp ((%%) _ {pos = Here}) = Nothing `Because` (Refl, TVar)
+  envSp ((%%) name {pos = There i}) =
+    let
+      (b ** prf) =
+        skipsStrengthens
+          {f = (indexAll i Env0).value.thins}
+          (rewrite getEnv0 i in Here)
+          _
+    in
+    Just b `Because` prf
+
+subAllWf envWf [<] = [<]
+subAllWf envWf (wfs :< wf) = subAllWf envWf wfs :< sub'Wf envWf wf
+
+export
+subWf :
+  {a : Ty ctx1} ->
+  {env : All (Assoc0 $ Ty ctx2) ctx1} ->
+  DAll (\ty => WellFormed ty) env ->
+  WellFormed a ->
+  WellFormed (sub env a)
+subWf envWf = sub'Wf (mapDProperty id envWf)