Introduce names in contexts.

Introduce rows for n-ary sums and products.

Remove union types.

8 files changed, 1612 insertions, 1695 deletions

diff --git a/inky.ipkg b/inky.ipkg
index 22902e4..b3d274f 100644
--- a/inky.ipkg
+++ b/inky.ipkg
@@ -9,6 +9,7 @@ depends = contrib
 modules
   = Data.Maybe.Decidable
   , Data.These.Decidable
+  , Inky.Context
   , Inky.Parser
   , Inky.Term
   , Inky.Term.Pretty
diff --git a/src/Inky/Context.idr b/src/Inky/Context.idr
new file mode 100644
index 0000000..b0393f3
--- /dev/null
+++ b/src/Inky/Context.idr
@@ -0,0 +1,605 @@
+module Inky.Context
+
+import public Data.Singleton
+import public Data.So
+
+import Data.Bool.Decidable
+import Data.Maybe.Decidable
+import Data.DPair
+import Data.Nat
+
+-- Contexts --------------------------------------------------------------------
+
+export
+infix 2 :-
+
+export
+prefix 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 (a : Type) where
+    constructor (:-)
+    0 name : String
+    value : a
+
+  public export
+  Functor Assoc0 where
+    map f x = x.name :- f x.value
+
+public export
+data Context : Type -> Type where
+  Lin : Context a
+  (:<) : Context a -> Assoc a -> Context a
+
+public export
+Functor Context where
+  map f [<] = [<]
+  map f (ctx :< x) = map f ctx :< map f x
+
+public export
+Foldable Context where
+  foldr f x [<] = x
+  foldr f x (ctx :< (_ :- y)) = foldr f (f y x) ctx
+
+  foldl f x [<] = x
+  foldl f x (ctx :< (_ :- y)) = f (foldl f x ctx) y
+
+  null [<] = True
+  null (ctx :< x) = False
+
+%name Context ctx
+
+public export
+data Length : Context a -> Type where
+  Z : Length [<]
+  S : Length ctx -> Length (ctx :< x)
+
+%name Length len
+
+public export
+(++) : Context a -> Context a -> Context a
+ctx ++ [<] = ctx
+ctx ++ ctx' :< x = (ctx ++ ctx') :< x
+
+export
+lengthAppend : Length ctx1 -> Length ctx2 -> Length (ctx1 ++ ctx2)
+lengthAppend len1 Z = len1
+lengthAppend len1 (S len2) = S (lengthAppend len1 len2)
+
+length : Context a -> Nat
+length [<] = 0
+length (ctx :< x) = S (length ctx)
+
+-- Variables -------------------------------------------------------------------
+
+public export
+data VarPos : Context a -> (0 x : String) -> a -> Type where
+  [search x]
+  Here : VarPos (ctx :< (x :- v)) x v
+  There : VarPos ctx x v -> VarPos (ctx :< y) x v
+
+public export
+record Var (ctx : Context a) (v : a) where
+  constructor (%%)
+  0 name : String
+  {auto pos : VarPos ctx name v}
+
+%name VarPos pos
+%name Var i, j, k
+
+public export
+toVar : VarPos ctx x v -> Var ctx v
+toVar pos = (%%) x {pos}
+
+public export
+toNat : VarPos ctx x v -> Nat
+toNat Here = 0
+toNat (There pos) = S (toNat pos)
+
+public export
+ThereVar : Var ctx v -> Var (ctx :< x) v
+ThereVar i = toVar (There i.pos)
+
+-- Basic Properties
+
+export
+thereCong :
+  {0 i : VarPos ctx x v} -> {0 j : VarPos ctx y v} -> i = j ->
+  There {y = z} i = There {y = z} j
+thereCong Refl = Refl
+
+export
+toVarCong : {0 i : VarPos ctx x v} -> {0 j : VarPos ctx y w} -> i = j -> toVar i = toVar j
+toVarCong Refl = Refl
+
+export
+toNatCong : {0 i : VarPos ctx x v} -> {0 j : VarPos ctx y w} -> i = j -> toNat i = toNat j
+toNatCong Refl = Refl
+
+export
+toNatCong' : {0 i, j : Var ctx v} -> i = j -> toNat i.pos = toNat j.pos
+toNatCong' Refl = Refl
+
+export
+toNatInjective : {i : VarPos ctx x v} -> {j : VarPos ctx y w} -> (0 _ : toNat i = toNat 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
+
+export
+toVarInjective : {i : VarPos ctx x v} -> {j : VarPos ctx y v} -> (0 _ : toVar i = toVar j) -> i = j
+toVarInjective prf = toNatInjective $ toNatCong' prf
+
+-- Decidable Equality
+
+export
+eq : Var ctx v -> Var ctx w -> Bool
+eq i j = toNat i.pos == toNat j.pos
+
+public export
+Eq (Var {a} ctx v) where
+  (==) = eq
+
+reflectPosEq :
+  (i : VarPos ctx x v) ->
+  (j : VarPos ctx y w) ->
+  (i = j) `Reflects` (toNat i == toNat j)
+reflectPosEq Here Here = RTrue Refl
+reflectPosEq Here (There j) = RFalse (\case Refl impossible)
+reflectPosEq (There i) Here = RFalse (\case Refl impossible)
+reflectPosEq (There i) (There j) with (reflectPosEq i j) | (toNat i == toNat j)
+  reflectPosEq (There i) (There .(i)) | RTrue Refl | _ = RTrue Refl
+  _ | RFalse neq | _ = RFalse (\case Refl => neq Refl)
+
+export
+reflectEq : (i : Var {a} ctx v) -> (j : Var ctx w) -> (i = j) `Reflects` (i `eq` j)
+reflectEq ((%%) x {pos = pos1}) ((%%) y {pos = pos2})
+  with (reflectPosEq pos1 pos2) | (toNat pos1 == toNat pos2)
+  _ | RTrue eq | _ = RTrue (toVarCong eq)
+  _ | RFalse neq | _ = RFalse (\case Refl => neq Refl)
+
+-- Weakening
+
+wknLPos : VarPos ctx1 x v -> Length ctx2 -> VarPos (ctx1 ++ ctx2) x v
+wknLPos pos Z = pos
+wknLPos pos (S len) = There (wknLPos pos len)
+
+wknRPos : VarPos ctx2 x v -> VarPos (ctx1 ++ ctx2) x v
+wknRPos Here = Here
+wknRPos (There pos) = There (wknRPos pos)
+
+splitPos : Length ctx2 -> VarPos (ctx1 ++ ctx2) x v -> Either (VarPos ctx1 x v) (VarPos ctx2 x v)
+splitPos Z pos = Left pos
+splitPos (S len) Here = Right Here
+splitPos (S len) (There pos) = mapSnd There $ splitPos len pos
+
+export
+wknL : {auto len : Length ctx2} -> Var ctx1 v -> Var (ctx1 ++ ctx2) v
+wknL i = toVar $ wknLPos i.pos len
+
+export
+wknR : Var ctx2 v -> Var (ctx1 ++ ctx2) v
+wknR i = toVar $ wknRPos i.pos
+
+export
+split : {auto len : Length ctx2} -> Var (ctx1 ++ ctx2) x -> Either (Var ctx1 x) (Var ctx2 x)
+split i = bimap toVar toVar $ splitPos len i.pos
+
+export
+lift :
+  {auto len : Length ctx} ->
+  (forall x. Var ctx1 x -> Var ctx2 x) ->
+  Var (ctx1 ++ ctx) x -> Var (ctx2 ++ ctx) x
+lift f = either (wknL {len} . f) wknR . split {len}
+
+-- Names
+
+nameOfPos : {ctx : Context a} -> VarPos ctx x v -> Singleton x
+nameOfPos Here = Val x
+nameOfPos (There pos) = nameOfPos pos
+
+export
+nameOf : {ctx : Context a} -> (i : Var ctx v) -> Singleton i.name
+nameOf i = nameOfPos i.pos
+
+-- Environments ----------------------------------------------------------------
+
+namespace Quantifier
+  public export
+  data All : (0 p : a -> Type) -> Context a -> Type where
+    Lin : All p [<]
+    (:<) :
+      All p ctx -> (px : Assoc0 (p x.value)) ->
+      {auto 0 prf : px.name = x.name}->
+      All p (ctx :< x)
+
+  %name Quantifier.All env
+
+  indexAllPos : VarPos ctx x v -> All p ctx -> p v
+  indexAllPos Here (env :< px) = px.value
+  indexAllPos (There pos) (env :< px) = indexAllPos pos env
+
+  export
+  indexAll : Var ctx v -> All p ctx -> p v
+  indexAll i env = indexAllPos i.pos env
+
+  export
+  mapProperty : ({0 x : a} -> p x -> q x) -> All p ctx -> All q ctx
+  mapProperty f [<] = [<]
+  mapProperty f (env :< (x :- px)) = mapProperty f env :< (x :- f px)
+
+  export
+  (++) : All p ctx1 -> All p ctx2 -> All p (ctx1 ++ ctx2)
+  env1 ++ [<] = env1
+  env1 ++ env2 :< px = (env1 ++ env2) :< px
+
+-- Rows ------------------------------------------------------------------------
+
+namespace Row
+  ||| Contexts where names are unique.
+  public export
+  data Row : Type -> Type
+
+  public export
+  freshIn : String -> Row a -> Bool
+
+  data Row where
+    Lin : Row a
+    (:<) : (row : Row a) -> (x : Assoc a) -> {auto 0 fresh : So (x.name `freshIn` row)} -> Row a
+
+  x `freshIn` [<] = True
+  x `freshIn` (row :< y) = x /= y.name && (x `freshIn` row)
+
+  %name Row row
+
+  public export
+  map : (a -> b) -> Row a -> Row b
+  export
+  0 mapFresh : (f : a -> b) -> (row : Row a) -> So (x `freshIn` row) -> So (x `freshIn` map f row)
+
+  map f [<] = [<]
+  map f ((:<) row x {fresh}) = (:<) (map f row) (map f x) {fresh = mapFresh f row fresh}
+
+  mapFresh f [<] = id
+  mapFresh f (row :< (y :- _)) = andSo . mapSnd (mapFresh f row) . soAnd
+
+  public export
+  Functor Row where
+    map = Row.map
+
+  public export
+  Foldable Row where
+    foldr f x [<] = x
+    foldr f x (row :< (_ :- y)) = foldr f (f y x) row
+
+    foldl f x [<] = x
+    foldl f x (row :< (_ :- y)) = f (foldl f x row) y
+
+    null [<] = True
+    null (row :< x) = False
+
+  ||| Forget the freshness of names.
+  public export
+  forget : Row a -> Context a
+  forget [<] = [<]
+  forget (row :< x) = forget row :< x
+
+  -- Equality --
+
+  soUnique : (x, y : So b) -> x = y
+  soUnique Oh Oh = Refl
+
+  export
+  snocCong2 :
+    {0 row1, row2 : Row a} -> row1 = row2 ->
+    {0 x, y : Assoc a} -> x = y ->
+    {0 fresh1 : So (x.name `freshIn` row1)} ->
+    {0 fresh2 : So (y.name `freshIn` row2)} ->
+    row1 :< x = row2 :< y
+  snocCong2 Refl Refl = rewrite soUnique fresh1 fresh2 in Refl
+
+  -- Variables aren't fresh --
+
+  -- NOTE: cannot implement
+  0 strEqReflect : (x, y : String) -> (x = y) `Reflects` (x == y)
+  strEqReflect x y = believe_me ()
+
+  0 strEqRefl : (x : String) -> Not (So (x /= x))
+  strEqRefl x prf with (strEqReflect x x) | (x == x)
+    _ | RTrue _ | _ = absurd prf
+    _ | RFalse neq | _ = neq Refl
+
+  export
+  0 varPosNotFresh : VarPos (forget row) x v -> Not (So (x `freshIn` row))
+  varPosNotFresh {row = row :< (x :- v)} Here fresh = strEqRefl x (fst $ soAnd fresh)
+  varPosNotFresh {row = row :< y} (There pos) fresh = varPosNotFresh pos (snd $ soAnd fresh)
+
+  export
+  varUniqueIndex : (row : Row a) -> VarPos (forget row) x v -> VarPos (forget row) x w -> v = w
+  varUniqueIndex (row :< (x :- _)) Here Here = Refl
+  varUniqueIndex ((:<) row (x :- _) {fresh}) Here (There pos2) = void $ varPosNotFresh pos2 fresh
+  varUniqueIndex ((:<) row (x :- _) {fresh}) (There pos1) Here = void $ varPosNotFresh pos1 fresh
+  varUniqueIndex (row :< (y :- _)) (There pos1) (There pos2) = varUniqueIndex row pos1 pos2
+
+  -- Equivalence --
+
+  export infix 6 <~>
+
+  public export
+  data Step : Row a -> Row a -> Type where
+    Cong :
+      Step row1 row2 -> (0 x : Assoc a) ->
+      {0 fresh1 : So (x.name `freshIn` row1)} ->
+      {0 fresh2 : So (x.name `freshIn` row2)} ->
+      Step (row1 :< x) (row2 :< x)
+    Swap :
+      (0 x : Assoc a) -> (0 y : Assoc a) ->
+      {0 fresh1 : So (x.name `freshIn` row)} ->
+      {0 fresh2 : So (y.name `freshIn` row :< x)} ->
+      {0 fresh3 : So (y.name `freshIn` row)} ->
+      {0 fresh4 : So (x.name `freshIn` row :< y)} ->
+      Step (row :< x :< y) (row :< y :< x)
+
+  public export
+  data (<~>) : Row a -> Row a -> Type where
+    Nil : row <~> row
+    (::) : Step row1 row2 -> row2 <~> row3 -> row1 <~> row3
+
+  %name Step step
+  %name (<~>) prf
+
+  export
+  trans : row1 <~> row2 -> row2 <~> row3 -> row1 <~> row3
+  trans [] prf = prf
+  trans (step :: prf1) prf2 = step :: trans prf1 prf2
+
+  symStep : Step row1 row2 -> Step row2 row1
+  symStep (Cong step x) = Cong (symStep step) x
+  symStep (Swap x y) = Swap y x
+
+  export
+  sym : row1 <~> row2 -> row2 <~> row1
+  sym [] = []
+  sym (step :: prf) = trans (sym prf) [symStep step]
+
+  equivLengthStep : Step row1 row2 -> length (forget row1) = length (forget row2)
+  equivLengthStep (Cong step x) = cong S (equivLengthStep step)
+  equivLengthStep (Swap x y) = Refl
+
+  equivLength : row1 <~> row2 -> length (forget row1) = length (forget row2)
+  equivLength [] = Refl
+  equivLength (step :: prf) = trans (equivLengthStep step) (equivLength prf)
+
+  export
+  Uninhabited ((:<) row x {fresh} <~> [<]) where
+    uninhabited prf = absurd (equivLength prf)
+
+  export
+  Uninhabited ([<] <~> (:<) row x {fresh}) where
+    uninhabited prf = absurd (equivLength prf)
+
+  0 equivFreshInStep : Step row1 row2 -> So (x `freshIn` row1) -> So (x `freshIn` row2)
+  equivFreshInStep (Cong step y) = andSo . mapSnd (equivFreshInStep step) . soAnd
+  equivFreshInStep (Swap {row} (y :- v) (z :- w)) =
+    andSo . mapSnd andSo .
+    (\(prf1, prf2, prf3) => (prf2, prf1, prf3)) .
+    mapSnd (soAnd {a = x /= y, b = freshIn x row}) . soAnd
+
+  0 equivFreshIn : row1 <~> row2 -> So (x `freshIn` row1) -> So (x `freshIn` row2)
+  equivFreshIn [] = id
+  equivFreshIn (step :: prf) = equivFreshIn prf . equivFreshInStep step
+
+  cong :
+    row1 <~> row2 -> (0 x : Assoc a) ->
+    {0 fresh1 : So (x.name `freshIn` row1)} ->
+    {0 fresh2 : So (x.name `freshIn` row2)} ->
+    row1 :< x <~> row2 :< x
+  cong [] x = rewrite soUnique fresh1 fresh2 in []
+  cong (step :: prf) x =
+    let 0 fresh' = equivFreshInStep step fresh1 in
+    Cong step x {fresh2 = fresh'} :: cong prf x
+
+  -- Removal --
+
+  public export
+  removePos : (row : Row a) -> VarPos (forget row) x v -> (Singleton v, Row a)
+  export
+  0 removePosFresh :
+    (row : Row a) -> (pos : VarPos (forget row) x v) ->
+    So (y `freshIn` row) -> So (y `freshIn` snd (removePos row pos))
+
+  removePos (row :< (_ :- v)) Here = (Val v, row)
+  removePos ((:<) row x {fresh}) (There pos) =
+    ( fst (removePos row pos)
+    , (:<) (snd $ removePos row pos) x {fresh = removePosFresh row pos fresh}
+    )
+
+  removePosFresh (row :< _) Here = snd . soAnd
+  removePosFresh ((:<) row (z :- v) {fresh}) (There pos) =
+    andSo . mapSnd (removePosFresh row pos) . soAnd
+
+  public export
+  remove : (row : Row a) -> Var (forget row) v -> (Singleton v, Row a)
+  remove row i = removePos row i.pos
+
+  -- Reflection
+
+  -- NOTE: cannot implement
+  0 soNotSym : {x, y : String} -> So (x /= y) -> So (y /= x)
+  soNotSym = believe_me
+
+  0 freshNotPos : (row : Row a) -> VarPos (forget row) x v -> So (y `freshIn` row) -> So (y /= x)
+  freshNotPos (row :< _) Here = fst . soAnd
+  freshNotPos (row :< x) (There pos) = freshNotPos row pos . snd . soAnd
+
+  export
+  0 removedIsFresh :
+    (row : Row a) -> (pos : VarPos (forget row) x v) ->
+    So (x `freshIn` snd (removePos row pos))
+  removedIsFresh ((:<) row _ {fresh}) Here = fresh
+  removedIsFresh ((:<) row (y :- v) {fresh}) (There pos) =
+    andSo (soNotSym (freshNotPos row pos fresh), removedIsFresh row pos)
+
+  export
+  reflectRemovePos :
+    (row : Row a) -> (pos : VarPos (forget row) x v) ->
+    (:<) (snd $ removePos row pos) (x :- v) {fresh = removedIsFresh row pos} <~> row
+  reflectRemovePos ((:<) row _ {fresh}) Here = []
+  reflectRemovePos ((:<) row (y :- w) {fresh}) (There pos) =
+    (  Swap (y :- w) (x :- v)
+         {fresh4 = andSo (freshNotPos row pos fresh, removePosFresh row pos fresh)}
+    :: cong (reflectRemovePos row pos) (y :- w))
+
+  -- Tracing Variables --
+
+  equivVarPosStep : Step row1 row2 -> VarPos (forget row1) x v -> VarPos (forget row2) x v
+  equivVarPosStep (Cong step _) Here = Here
+  equivVarPosStep (Cong step y) (There pos) = There (equivVarPosStep step pos)
+  equivVarPosStep (Swap y _) Here = There Here
+  equivVarPosStep (Swap _ z) (There Here) = Here
+  equivVarPosStep (Swap y z) (There (There pos)) = There (There pos)
+
+  export
+  equivVarPos : row1 <~> row2 -> VarPos (forget row1) x v -> VarPos (forget row2) x v
+  equivVarPos [] = id
+  equivVarPos (step :: prf) = equivVarPos prf . equivVarPosStep step
+
+  removePosInjectiveStep :
+    (prf : Step row1 row2) -> (pos : VarPos (forget row1) x v) ->
+    snd (removePos row1 pos) <~> snd (removePos row2 (equivVarPosStep prf pos))
+  removePosInjectiveStep (Cong step _) Here = [step]
+  removePosInjectiveStep (Cong step (y :- v)) (There pos) =
+    cong (removePosInjectiveStep step pos) (y :- v)
+  removePosInjectiveStep (Swap (y :- v) _) Here = cong [] (y :- v)
+  removePosInjectiveStep (Swap _ (z :- v)) (There Here) = cong [] (z :- v)
+  removePosInjectiveStep (Swap (y :- v) (z :- w)) (There (There pos)) = [Swap (y :- v) (z :- w)]
+
+  export
+  removePosInjective :
+    (prf : row1 <~> row2) -> (pos : VarPos (forget row1) x v) ->
+    snd (removePos row1 pos) <~> snd (removePos row2 (equivVarPos prf pos))
+  removePosInjective [] pos = []
+  removePosInjective (step :: prf) pos =
+    trans (removePosInjectiveStep step pos) (removePosInjective prf $ equivVarPosStep step pos)
+
+  export
+  equivVarUnique :
+    {0 fresh1 : So (x `freshIn` row1)} ->
+    {0 fresh2 : So (x `freshIn` row2)} ->
+    (prf : row1 :< (x :- v) <~> row2 :< (x :- v)) ->
+    equivVarPos prf Here = Here
+  equivVarUnique prf with (equivVarPos prf Here)
+    _ | Here = Refl
+    _ | There pos = void $ varPosNotFresh pos fresh2
+
+  -- Partial Removal --
+
+  FreshOrNothing : String -> Maybe (a, Row a) -> Type
+  FreshOrNothing x Nothing = ()
+  FreshOrNothing x (Just (a, row)) = So (x `freshIn` row)
+
+  removeHelper :
+    (m : Maybe (a, Row a)) -> (x : Assoc a) ->
+    (0 fresh : FreshOrNothing x.name m) ->
+    Maybe (a, Row a)
+  removeHelper Nothing x fresh = Nothing
+  removeHelper (Just (v, row)) x fresh = Just (v, row :< x)
+
+  ||| Attempt to remove the value at name `x` from the row.
+  export
+  remove' : String -> Row a -> Maybe (a, Row a)
+  removeFresh :
+    (x : String) -> (row : Row a) ->
+    {y : String} -> So (y `freshIn` row) -> FreshOrNothing y (remove' x row)
+
+  remove' x [<] = Nothing
+  remove' x ((:<) row (y :- v) {fresh}) =
+    if y == x
+    then Just (v, row)
+    else removeHelper (remove' x row) (y :- v) (removeFresh x row fresh)
+
+  removeFresh x [<] prf = ()
+  removeFresh x (row :< (y :- v)) {y = z} prf with (y == x)
+    _ | True = snd (soAnd prf)
+    _ | False with (removeFresh x row $ snd $ soAnd prf) | (remove' x row)
+      _ | _ | Nothing = ()
+      _ | prf' | Just (v', row') = andSo (fst (soAnd prf), prf')
+
+  -- Reflection
+
+  notSoToSoNot : {b : Bool} -> Not (So b) -> So (not b)
+  notSoToSoNot {b = False} nprf = Oh
+  notSoToSoNot {b = True} nprf = absurd (nprf Oh)
+
+  0 reflectRemoveHelper : {x, y : String} -> Not (x = y) -> Not (So (x == y))
+  reflectRemoveHelper neq eq with (strEqReflect x y) | (x == y)
+    reflectRemoveHelper neq Oh | RTrue eq | _ = neq eq
+
+  reflectRemoveHelper' :
+    {0 fresh1 : So (y `freshIn` row1)} ->
+    (x : String) -> Not (y = x) ->
+    (0 fresh2 : So (x `freshIn` row2)) -> (prf : row1 :< (y :- v) <~> row2 :< (x :- v')) ->
+    (  pos : VarPos (forget row2) y v
+    ** snd (removePos (row2 :< (x :- v')) (equivVarPos prf Here)) <~>
+           (:<) (snd (removePos row2 pos)) (x :- v')
+             {fresh = removePosFresh row2 pos {y = x} fresh2})
+  reflectRemoveHelper' x neq fresh2 prf with (equivVarPos prf Here)
+    reflectRemoveHelper' x neq fresh2 prf | Here = absurd (neq Refl)
+    reflectRemoveHelper' x neq fresh2 prf | There pos =
+      (pos ** [])
+
+  public export
+  Remove : String -> Row a -> a -> Row a -> Type
+  Remove x row v row' =
+    Exists {type = So (x `freshIn` row')} (\fresh => row <~> row' :< (x :- v))
+
+  export
+  removeUnique :
+    (x : String) -> (row1 : Row a) ->
+    Remove x row1 v row2 -> Remove x row1 w row3 -> (v = w, row2 <~> row3)
+  removeUnique x row1 (Evidence fresh1 prf1) (Evidence fresh2 prf2) =
+    let eq = varUniqueIndex row1 (equivVarPos (sym prf1) Here) (equivVarPos (sym prf2) Here) in
+    let
+      prf : row2 :< (x :- v) <~> row3 :< (x :- v)
+      prf = trans (sym prf1) (rewrite eq in prf2)
+    in
+    ( eq
+    , replace
+        {p = \pos => row2 <~> snd (removePos (row3 :< (x :- v)) pos)}
+        (equivVarUnique prf)
+        (removePosInjective prf Here))
+
+  export
+  0 reflectRemove :
+    (x : String) -> (row : Row a) ->
+    uncurry (Remove x row) `OnlyWhen` remove' x row
+  reflectRemove x [<] = RNothing (\(v, row), (Evidence _ prf) => absurd prf)
+  reflectRemove x ((:<) row (y :- v) {fresh}) with (strEqReflect y x) | (y == x)
+    _ | RTrue eq | _ = rewrite sym eq in RJust (Evidence fresh [])
+    _ | RFalse neq | _ with (reflectRemove x row, removeFresh x row {y}) | (remove' x row)
+      _ | (RJust (Evidence fresh' prf), mkFresh) | Just (v', row') =
+        RJust (Evidence
+          (andSo (notSoToSoNot (reflectRemoveHelper (\eq => neq $ sym eq)), fresh'))
+          (trans
+            (cong prf (y :- v)
+              {fresh2 = andSo (notSoToSoNot (reflectRemoveHelper neq), mkFresh fresh)})
+            [Swap (x :- v') (y :- v)]))
+      _ | (RNothing nprf, mkFresh) | _ =
+        RNothing (\(v', row'), (Evidence fresh' prf) =>
+          let (pos ** prf') = reflectRemoveHelper' x neq fresh' prf in
+          void $
+          nprf (v', snd (remove row' ((%%) y {pos}))) $
+          Evidence
+            (removePosFresh row' pos fresh')
+            (trans (removePosInjective prf Here) prf'))
diff --git a/src/Inky/Parser.idr b/src/Inky/Parser.idr
index 047165c..1ad48d8 100644
--- a/src/Inky/Parser.idr
+++ b/src/Inky/Parser.idr
@@ -7,116 +7,9 @@ import Data.List.Elem
 import Data.List1
 import Data.Nat
 import Data.So
+import Inky.Context
+import Text.Lexer
 
--- Contexts --------------------------------------------------------------------
-
-export
-infix 2 :-
-
-export
-prefix 2 %%
-
-public export
-record Assoc (a : Type) where
-  constructor (:-)
-  0 name : String
-  value : a
-
-public export
-data Context : Type -> Type where
-  Lin : Context a
-  (:<) : Context a -> Assoc a -> Context a
-
-%name Context ctx
-
-public export
-data Length : Context a -> Type where
-  Z : Length [<]
-  S : Length ctx -> Length (ctx :< x)
-
-%name Length len
-
-public export
-(++) : Context a -> Context a -> Context a
-ctx ++ [<] = ctx
-ctx ++ ctx' :< x = (ctx ++ ctx') :< x
-
-lengthAppend : Length ctx1 -> Length ctx2 -> Length (ctx1 ++ ctx2)
-lengthAppend len1 Z = len1
-lengthAppend len1 (S len2) = S (lengthAppend len1 len2)
-
--- Variableents
-
-public export
-data VariablePos : Context a -> (0 x : String) -> a -> Type where
-  [search x]
-  Here : VariablePos (ctx :< (x :- v)) x v
-  There : VariablePos ctx x v -> VariablePos (ctx :< y) x v
-
-public export
-record Variable (ctx : Context a) (v : a) where
-  constructor (%%)
-  0 name : String
-  {auto pos : VariablePos ctx name v}
-
-toVar : VariablePos ctx x v -> Variable ctx v
-toVar pos = (%%) x {pos}
-
-wknLPos : VariablePos ctx1 x v -> Length ctx2 -> VariablePos (ctx1 ++ ctx2) x v
-wknLPos x Z = x
-wknLPos x (S len) = There (wknLPos x len)
-
-wknRPos : VariablePos ctx2 x v -> VariablePos (ctx1 ++ ctx2) x v
-wknRPos Here = Here
-wknRPos (There x) = There (wknRPos x)
-
-splitPos : Length ctx2 -> VariablePos (ctx1 ++ ctx2) x v -> Either (VariablePos ctx1 x v) (VariablePos ctx2 x v)
-splitPos Z x = Left x
-splitPos (S len) Here = Right Here
-splitPos (S len) (There x) = mapSnd There $ splitPos len x
-
-wknL : {auto len : Length ctx2} -> Variable ctx1 v -> Variable (ctx1 ++ ctx2) v
-wknL x = (%%) x.name {pos = wknLPos x.pos len}
-
-wknR : Variable ctx2 v -> Variable (ctx1 ++ ctx2) v
-wknR x = (%%) x.name {pos = wknRPos x.pos}
-
-split : {auto len : Length ctx2} -> Variable (ctx1 ++ ctx2) x -> Either (Variable ctx1 x) (Variable ctx2 x)
-split x = bimap toVar toVar $ splitPos len x.pos
-
-lift :
-  {auto len : Length ctx} ->
-  (forall x. Variable ctx1 x -> Variable ctx2 x) ->
-  Variable (ctx1 ++ ctx) x -> Variable (ctx2 ++ ctx) x
-lift f = either (wknL {len} . f) wknR . split {len}
-
--- Environments
-
-namespace Quantifier
-  public export
-  data All : (0 p : a -> Type) -> Context a -> Type where
-    Lin : All p [<]
-    (:<) : All p ctx -> (px : p x.value) -> All p (ctx :< x)
-
-  %name Quantifier.All env
-
-  indexAllPos : VariablePos ctx x v -> All p ctx -> p v
-  indexAllPos Here (env :< px) = px
-  indexAllPos (There x) (env :< px) = indexAllPos x env
-
-  export
-  indexAll : Variable ctx v -> All p ctx -> p v
-  indexAll x env = indexAllPos x.pos env
-
-  export
-  mapProperty : ({0 x : a} -> p x -> q x) -> All p ctx -> All q ctx
-  mapProperty f [<] = [<]
-  mapProperty f (env :< px) = mapProperty f env :< f px
-
-  export
-  (++) : All p ctx1 -> All p ctx2 -> All p (ctx1 ++ ctx2)
-  env1 ++ [<] = env1
-  env1 ++ env2 :< px = (env1 ++ env2) :< px
 
 -- Parser Expressions ----------------------------------------------------------
 
@@ -131,10 +24,10 @@ linUnless True ctx = ctx
 
 public export
 data Parser : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> Type -> Type where
-  Var : (f : a -> b) -> Variable free (nil, a) -> Parser i nil locked free b
+  Var : (f : a -> b) -> Var free (nil, a) -> Parser i nil locked free b
   Fail : (msg : String) -> Parser i False locked free a
   Empty : (x : a) -> Parser i True locked free a
-  Lit : (text : i) -> (x : a) -> Parser i False locked free a
+  Lit : (text : i) -> (x : String -> a) -> Parser i False locked free a
   (<**>) :
     {nil1, nil2 : Bool} ->
     Parser i nil1 locked free (a -> b) ->
@@ -158,7 +51,7 @@ Functor (Parser i nil locked free) where
   map f (Var g x) = Var (f . g) x
   map f (Fail msg) = Fail msg
   map f (Empty x) = Empty (f x)
-  map f (Lit text x) = Lit text (f x)
+  map f (Lit text g) = Lit text (f . g)
   map f ((<**>) {nil1 = True} p q) = map (f .) p <**> q
   map f ((<**>) {nil1 = False} p q) = map (f .) p <**> q
   map f (p <|> q) = map f p <|> map f q
@@ -209,7 +102,7 @@ follow penv1 penv2 fenv1 fenv2 (Fix x f p) =
   -- Proof:
   --   - we always add information
   --   - no step depends on existing information
-  follow (penv1 :< peek penv2 p) penv2 (fenv1 :< empty) fenv2 p
+  follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- empty)) fenv2 p
 
 export
 WellTyped :
@@ -246,8 +139,8 @@ WellTyped penv1 penv2 fenv1 fenv2 (p <|> q) =
   )
 WellTyped penv1 penv2 fenv1 fenv2 (Fix x f p) =
   let fst = peek penv2 p in
-  let flw = follow (penv1 :< fst) penv2 (fenv1 :< empty) fenv2 p in
-  WellTyped (penv1 :< fst) penv2 (fenv1 :< flw) fenv2 p
+  let flw = follow (penv1 :< (x :- fst)) penv2 (fenv1 :< (x :- empty)) fenv2 p in
+  WellTyped (penv1 :< (x :- fst)) penv2 (fenv1 :< (x :- flw)) fenv2 p
 
 -- Parsing Function ------------------------------------------------------------
 
@@ -320,9 +213,9 @@ parser :
   (fenv1 : _) ->
   (fenv2 : _) ->
   {auto 0 wf : WellTyped penv1 penv2 fenv1 fenv2 p} ->
-  (xs : List i) ->
-  All (\x => (ys : List i) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked ->
-  All (\x => (ys : List i) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free ->
+  (xs : List (WithBounds (Token i))) ->
+  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked ->
+  All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free ->
   M xs nil a
 parser (Var f x) penv1 penv2 fenv1 fenv2 xs env1 env2 =
   f <$> indexAll x env2 xs (Lax reflexive)
@@ -330,13 +223,13 @@ parser (Fail msg) penv1 penv2 fenv1 fenv2 xs env1 env2 =
   Err msg
 parser (Empty x) penv1 penv2 fenv1 fenv2 xs env1 env2 =
   Ok x xs (Lax reflexive)
-parser (Lit text x) penv1 penv2 fenv1 fenv2 xs env1 env2 =
+parser (Lit text f) penv1 penv2 fenv1 fenv2 xs env1 env2 =
   case xs of
     [] => Err "expected \{text}, got end of file"
     y :: ys =>
-      if y == text
-      then Ok x ys (Strict reflexive)
-      else Err "expected \{text}, got \{y}"
+      if y.val.kind == text
+      then Ok (f y.val.text) ys (Strict reflexive)
+      else Err "\{show y.bounds}: expected \{text}, got \{y.val.kind}"
 parser ((<**>) {nil1 = False, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 =
   case parser p penv1 penv2 fenv1 fenv2 xs env1 env2 of
     Err msg => Err msg
@@ -372,15 +265,15 @@ parser ((<|>) {nil1, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 =
       then parser q penv1 penv2 fenv1 fenv2 [] env1 env2
       else Err "unexpected end of input"
     x :: xs =>
-      if elem x (peek penv2 p)
+      if elem x.val.kind (peek penv2 p)
       then wknL (parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2) nil2
-      else if elem x (peek penv2 q)
+      else if elem x.val.kind (peek penv2 q)
       then wknR nil1 (parser q penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2)
       else if nil1
       then parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2
       else if nil2
       then parser q penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2
-      else Err "unexpected token \{x}"
+      else Err "\{show x.bounds}: unexpected \{x.val.kind}"
 parser (Fix {a, b, nil} x f p) penv1 penv2 fenv1 fenv2 xs env1 env2 =
   let g = parser p _ _ _ _ {wf} in
   let
@@ -390,7 +283,7 @@ parser (Fix {a, b, nil} x f p) penv1 penv2 fenv1 fenv2 xs env1 env2 =
         (\ys, rec, lte =>
           g ys
             (  mapProperty (\f, zs, 0 prf => f zs $ transX prf lte) env1
-            :< (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte))
+            :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte)))
             )
             (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2))
         xs
@@ -403,7 +296,7 @@ parse :
   Eq i => Interpolation i =>
   (p : Parser i nil [<] [<] a) ->
   {auto 0 wf : WellTyped [<] [<] [<] [<] p} ->
-  (xs : List i) -> M xs nil a
+  (xs : List (WithBounds (Token i))) -> M xs nil a
 parse p xs = parser p [<] [<] [<] [<] xs [<] [<]
 
 -- Weakening -------------------------------------------------------------------
@@ -412,8 +305,8 @@ public export
 rename :
   (len1 : Length locked1) ->
   (len2 : Length locked2) ->
-  (forall x. Variable locked1 x -> Variable locked2 x) ->
-  (forall x. Variable free1 x -> Variable free2 x) ->
+  (forall x. Var locked1 x -> Var locked2 x) ->
+  (forall x. Var free1 x -> Var free2 x) ->
   Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a
 rename len1 len2 ren1 ren2 (Var f x) = Var f (ren2 x)
 rename len1 len2 ren1 ren2 (Fail msg) = Fail msg
@@ -430,6 +323,27 @@ rename len1 len2 ren1 ren2 (Fix x f p) =
   Fix x f (rename (S len1) (S len2) (lift {len = S Z} ren1) ren2 p)
 
 public export
+weaken :
+  (len1 : Length free2) ->
+  {auto len2 : Length locked} ->
+  Parser i nil (free2 ++ locked) free1 a -> Parser i nil locked (free1 ++ free2) a
+weaken len1 (Var f x) = Var f (wknL x)
+weaken len1 (Fail msg) = Fail msg
+weaken len1 (Empty x) = Empty x
+weaken len1 (Lit text x) = Lit text x
+weaken len1 ((<**>) {nil1 = False} p q) =
+  weaken len1 p <**>
+  rename Z Z
+    id
+    ( either (wknL . wknL) (either (wknL . wknR) wknR . split)
+    . split {len = lengthAppend len1 len2}
+    )
+    q
+weaken len1 ((<**>) {nil1 = True} p q) = weaken len1 p <**> weaken len1 q
+weaken len1 (p <|> q) = weaken len1 p <|> weaken len1 q
+weaken len1 (Fix x f p) = Fix x f (weaken len1 p)
+
+public export
 shift :
   {auto len1 : Length locked1} ->
   (len2 : Length locked2) ->
@@ -465,15 +379,8 @@ public export
 p <** q = const <$> p <**> q
 
 public export
-match : i -> Parser i False locked free ()
-match x = Lit x ()
-
-public export
-oneOf : (xs : List i) -> {auto 0 _ : NonEmpty xs} -> Parser i False locked free (x ** Elem x xs)
-oneOf [x] = (x ** Here) <$ match x
-oneOf (x :: xs@(_ :: _)) =
-  (x ** Here) <$ match x <|>
-  (\y => (y.fst ** There y.snd)) <$> oneOf xs
+match : TokenKind i => (kind : i) -> Parser i False locked free (TokType kind)
+match kind = Lit kind (tokValue kind)
 
 public export
 option : Parser i False locked free a -> Parser i True locked free (Maybe a)
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index f6e095c..d80ce77 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -2,60 +2,54 @@ module Inky.Term
 
 import Data.Bool.Decidable
 import Data.DPair
-import Data.List.Elem
 import Data.Maybe.Decidable
-import Data.These
-import Data.Vect
+import Data.List
+import Inky.Context
 import Inky.Thinning
 import Inky.Type
 
--- Redefine so I can prove stuff about it
-%hide
-Prelude.getAt
-
-getAt : Nat -> List a -> Maybe a
-getAt k [] = Nothing
-getAt 0 (x :: xs) = Just x
-getAt (S k) (x :: xs) = getAt k xs
-
 --------------------------------------------------------------------------------
 -- Definition ------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 public export
-data SynthTerm : Nat -> Nat -> Type
+data SynthTerm : (tyCtx, tmCtx : Context ()) -> Type
 public export
-data CheckTerm : Nat -> Nat -> Type
+data CheckTerm : (tyCtx, tmCtx : Context ()) -> Type
 
 data SynthTerm where
-  Var : Fin tm -> SynthTerm ty tm
-  Lit : Nat -> SynthTerm ty tm
-  Suc : CheckTerm ty tm -> SynthTerm ty tm
-  App : SynthTerm ty tm -> List1 (CheckTerm ty tm) -> SynthTerm ty tm
-  Prj : SynthTerm ty tm -> Nat -> SynthTerm ty tm
-  Expand : SynthTerm ty tm -> SynthTerm ty tm
-  Annot : CheckTerm ty tm -> Ty ty -> SynthTerm ty tm
+  Var : Var tmCtx v -> SynthTerm tyCtx tmCtx
+  Lit : Nat -> SynthTerm tyCtx tmCtx
+  Suc : CheckTerm tyCtx tmCtx -> SynthTerm tyCtx tmCtx
+  App :
+    SynthTerm tyCtx tmCtx ->
+    (args : List (CheckTerm tyCtx tmCtx)) ->
+    {auto 0 _ : NonEmpty args} ->
+    SynthTerm tyCtx tmCtx
+  Prj : SynthTerm tyCtx tmCtx -> String -> SynthTerm tyCtx tmCtx
+  Expand : SynthTerm tyCtx tmCtx -> SynthTerm tyCtx tmCtx
+  Annot : CheckTerm tyCtx tmCtx -> Ty tyCtx () -> SynthTerm tyCtx tmCtx
 
 data CheckTerm where
   Let :
-    SynthTerm ty tm ->
-    CheckTerm ty (S tm) ->
-    CheckTerm ty tm
-  Abs : (k : Nat) -> CheckTerm ty (S k + tm) -> CheckTerm ty tm
-  Inj : Nat -> CheckTerm ty tm -> CheckTerm ty tm
-  Tup : List (CheckTerm ty tm) -> CheckTerm ty tm
+    (x : String) -> SynthTerm tyCtx tmCtx ->
+    CheckTerm tyCtx (tmCtx :< (x :- ())) ->
+    CheckTerm tyCtx tmCtx
+  Abs : (bound : Context ()) -> CheckTerm tyCtx (tmCtx ++ bound) -> CheckTerm tyCtx tmCtx
+  Inj : String -> CheckTerm tyCtx tmCtx -> CheckTerm tyCtx tmCtx
+  Tup : Context (CheckTerm tyCtx tmCtx) -> CheckTerm tyCtx tmCtx
   Case :
-    SynthTerm ty tm ->
-    List (CheckTerm ty (S tm)) ->
-    CheckTerm ty tm
-  Contract : CheckTerm ty tm -> CheckTerm ty tm
+    SynthTerm tyCtx tmCtx ->
+    Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) ->
+    CheckTerm tyCtx tmCtx
+  Contract : CheckTerm tyCtx tmCtx -> CheckTerm tyCtx tmCtx
   Fold :
-    SynthTerm ty tm ->
-    CheckTerm ty (S tm) ->
-    CheckTerm ty tm
+    SynthTerm tyCtx tmCtx ->
+    (x : String) -> CheckTerm tyCtx (tmCtx :< (x :- ())) ->
+    CheckTerm tyCtx tmCtx
   Embed :
-    SynthTerm ty tm ->
-    CheckTerm ty tm
+    SynthTerm tyCtx tmCtx ->
+    CheckTerm tyCtx tmCtx
 
 %name SynthTerm e
 %name CheckTerm t, u, v
@@ -64,639 +58,670 @@ data CheckTerm where
 -- Well Formed -----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
-GetAt : Nat -> List a -> a -> Type
-GetAt k xs x = (n : Elem x xs ** elemToNat n = k)
+-- Lookup name in a row --------------------------------------------------------
+
+GetAt : String -> Row a -> a -> Type
+GetAt x ys y = VarPos (forget ys) x y
 
-CanProject : Ty ty -> List (Ty ty) -> Type
-CanProject (TUnion as) bs = forget as = bs
-CanProject (TProd as) bs = as = bs
-CanProject _ bs = Void
+getAtUnique :
+  (x : String) -> (ys : Row a) ->
+  GetAt x ys y -> GetAt x ys z -> y = z
+getAtUnique x (row :< (x :- b)) Here Here = Refl
+getAtUnique x ((:<) row (x :- a) {fresh}) Here (There pos2) = void $ varPosNotFresh pos2 fresh
+getAtUnique x ((:<) row (x :- b) {fresh}) (There pos1) Here = void $ varPosNotFresh pos1 fresh
+getAtUnique x (row :< (y :- v)) (There pos1) (There pos2) = getAtUnique x row pos1 pos2
+
+getAt : String -> Row a -> Maybe a
+getAt x as = fst <$> remove' x as
+
+0 reflectGetAt : (x : String) -> (ys : Row a) -> GetAt x ys `OnlyWhen` getAt x ys
+reflectGetAt x ys with (reflectRemove x ys) | (remove' x ys)
+  _ | RJust (Evidence fresh prf) | Just (y, _) = RJust (equivVarPos (sym prf) Here)
+  _ | RNothing nprf | _ =
+    RNothing (\y, pos =>
+      nprf (y, snd (removePos ys pos)) $
+      Evidence (removedIsFresh ys pos) (sym $ reflectRemovePos ys pos))
+
+-- Test if we have an arrow ----------------------------------------------------
+
+IsArrow : Ty tyCtx () -> Ty tyCtx () -> Ty tyCtx () -> Type
+IsArrow (TArrow a b) c d = (c = a, d = b)
+IsArrow _ c d = Void
+
+isArrowUnique : (a : Ty tyCtx ()) -> IsArrow a b c -> IsArrow a d e -> (b = d, c = e)
+isArrowUnique (TArrow a b) (Refl, Refl) (Refl, Refl) = (Refl, Refl)
+
+isArrow : Ty tyCtx () -> Maybe (Ty tyCtx (), Ty tyCtx ())
+isArrow (TArrow a b) = Just (a, b)
+isArrow _ = Nothing
+
+reflectIsArrow : (a : Ty tyCtx ()) -> uncurry (IsArrow a) `OnlyWhen` isArrow a
+reflectIsArrow (TArrow a b) = RJust (Refl, Refl)
+reflectIsArrow (TVar i) = RNothing (\(_, _), x => x)
+reflectIsArrow TNat = RNothing (\(_, _), x => x)
+reflectIsArrow (TProd as) = RNothing (\(_, _), x => x)
+reflectIsArrow (TSum as) = RNothing (\(_, _), x => x)
+reflectIsArrow (TFix x a) = RNothing (\(_, _), x => x)
+
+-- Test if we have a product ---------------------------------------------------
+
+IsProduct : Ty tyCtx () -> Row (Ty tyCtx ()) -> Type
+IsProduct (TProd as) bs = bs = as
+IsProduct _ bs = Void
 
-CanInject : Ty ty -> List (Ty ty) -> Type
-CanInject (TUnion as) bs = forget as = bs
-CanInject (TSum as) bs = as = bs
-CanInject _ bs = Void
+isProductUnique : (a : Ty tyCtx ()) -> IsProduct a as -> IsProduct a bs -> as = bs
+isProductUnique (TProd as) Refl Refl = Refl
 
-IsFixpoint : Ty ty -> Ty (S ty) -> Type
-IsFixpoint TNat b = b = TSum [TProd [], TVar FZ]
-IsFixpoint (TFix a) b = a = b
-IsFixpoint _ b = Void
+isProduct : Ty tyCtx () -> Maybe (Row (Ty tyCtx ()))
+isProduct (TProd as) = Just as
+isProduct _ = Nothing
 
-IsArrow : {ty : Nat} -> (k : Nat) -> Ty ty -> Vect k (Ty ty) -> Ty ty -> Type
-IsArrow 0 a as b = (as = [], b = a)
-IsArrow (S k) (TArrow dom cod) as b = (bs ** (as = dom :: bs, IsArrow k cod bs b))
-IsArrow (S k) _ as b = Void
+reflectIsProduct : (a : Ty tyCtx ()) -> IsProduct a `OnlyWhen` isProduct a
+reflectIsProduct (TVar i) = RNothing (\_, x => x)
+reflectIsProduct TNat = RNothing (\_, x => x)
+reflectIsProduct (TArrow a b) = RNothing (\_, x => x)
+reflectIsProduct (TProd as) = RJust Refl
+reflectIsProduct (TSum as) = RNothing (\_, x => x)
+reflectIsProduct (TFix x a) = RNothing (\_, x => x)
 
-IsProduct : Ty ty -> List (Ty ty) -> Type
-IsProduct (TProd as) bs = as = bs
-IsProduct _ bs = Void
+-- Test if we have a sum -------------------------------------------------------
 
-IsSum : Ty ty -> List (Ty ty) -> Type
-IsSum (TSum as) bs = as = bs
+IsSum : Ty tyCtx () -> Row (Ty tyCtx ()) -> Type
+IsSum (TSum as) bs = bs = as
 IsSum _ bs = Void
 
+isSumUnique : (a : Ty tyCtx ()) -> IsSum a as -> IsSum a bs -> as = bs
+isSumUnique (TSum as) Refl Refl = Refl
+
+isSum : Ty tyCtx () -> Maybe (Row (Ty tyCtx ()))
+isSum (TSum as) = Just as
+isSum _ = Nothing
+
+reflectIsSum : (a : Ty tyCtx ()) -> IsSum a `OnlyWhen` isSum a
+reflectIsSum (TVar i) = RNothing (\_, x => x)
+reflectIsSum TNat = RNothing (\_, x => x)
+reflectIsSum (TArrow a b) = RNothing (\_, x => x)
+reflectIsSum (TProd as) = RNothing (\_, x => x)
+reflectIsSum (TSum as) = RJust Refl
+reflectIsSum (TFix x a) = RNothing (\_, x => x)
+
+-- Test if we have a fixpoint --------------------------------------------------
+
+IsFixpoint : Ty tyCtx () -> (x ** Ty (tyCtx :< (x :- ())) ()) -> Type
+IsFixpoint TNat yb = (fst yb = "X", snd yb = TSum [<"Z" :- TProd [<], "S" :- TVar (%% fst yb)])
+IsFixpoint (TFix x a) yb = (prf : (fst yb = x) ** (snd yb = (rewrite prf in a)))
+IsFixpoint _ yb = Void
+
+isFixpointUnique : (a : Ty tyCtx ()) -> IsFixpoint a xb -> IsFixpoint a yc -> xb = yc
+isFixpointUnique TNat {xb = (_ ** _), yc = (_ ** _)} (Refl, Refl) (Refl, Refl) = Refl
+isFixpointUnique (TFix x a) {xb = (x ** a), yc = (x ** a)} (Refl ** Refl) (Refl ** Refl) = Refl
+
+isFixpoint : Ty tyCtx () -> Maybe (x ** Ty (tyCtx :< (x :- ())) ())
+isFixpoint TNat = Just ("X" ** TSum [<("Z" :- TProd [<]), ("S" :- TVar (%% "X"))])
+isFixpoint (TFix x a) = Just (x ** a)
+isFixpoint _ = Nothing
+
+reflectIsFixpoint : (a : Ty tyCtx ()) -> IsFixpoint a `OnlyWhen` isFixpoint a
+reflectIsFixpoint (TVar i) = RNothing (\_, x => x)
+reflectIsFixpoint TNat = RJust (Refl, Refl)
+reflectIsFixpoint (TArrow a b) = RNothing (\_, x => x)
+reflectIsFixpoint (TProd as) = RNothing (\_, x => x)
+reflectIsFixpoint (TSum as) = RNothing (\_, x => x)
+reflectIsFixpoint (TFix x a) = RJust (Refl ** Refl)
+
+-- Test if we have a function, collecting the bound types ----------------------
+
+IsFunction :
+  {tyCtx : Context ()} ->
+  (bound : Context ()) -> (fun : Ty tyCtx ()) ->
+  (dom : All (const $ Ty tyCtx ()) bound) -> (cod : Ty tyCtx ()) ->
+  Type
+IsFunction [<] fun dom cod = (dom = [<], cod = fun)
+IsFunction (bound :< (x :- ())) fun dom cod =
+  ( b ** c **
+  ( IsArrow fun b c
+  , ( dom' **
+    ( dom = dom' :< (x :- b)
+    , IsFunction bound c dom' cod
+    ))
+  ))
+
+
+isFunctionUnique :
+  (bound : Context ()) -> (a : Ty tyCtx ()) ->
+  forall dom1, dom2, cod1, cod2.
+  IsFunction bound a dom1 cod1 -> IsFunction bound a dom2 cod2 -> (dom1 = dom2, cod1 = cod2)
+isFunctionUnique [<] a (Refl, Refl) (Refl, Refl) = (Refl, Refl)
+isFunctionUnique (bound :< (x :- ())) a
+  (b1 ** c1 ** (isArrow1, (dom1' ** (Refl, isFunc1))))
+  (b2 ** c2 ** (isArrow2, (dom2' ** (Refl, isFunc2))))
+  with (isArrowUnique a isArrow1 isArrow2)
+  isFunctionUnique (bound :< (x :- ())) a
+    (b ** c ** (_, (dom1' ** (Refl, isFunc1))))
+    (b ** c ** (_, (dom2' ** (Refl, isFunc2))))
+    | (Refl, Refl)
+    with (isFunctionUnique bound c isFunc1 isFunc2)
+    isFunctionUnique (bound :< (x :- ())) a
+      (b ** c ** (_, (dom' ** (Refl, _))))
+      (b ** c ** (_, (dom' ** (Refl, _))))
+      | (Refl, Refl) | (Refl, Refl) = (Refl, Refl)
+
+isFunction :
+  (bound : Context ()) -> Ty tyCtx () ->
+  Maybe (All (const $ Ty tyCtx ()) bound, Ty tyCtx ())
+isFunction [<] a = Just ([<], a)
+isFunction (bound :< (x :- ())) a = do
+  (b, c) <- isArrow a
+  (dom, cod) <- isFunction bound c
+  Just (dom :< (x :- b), cod)
+
+reflectIsFunction :
+  (bound : Context ()) -> (a : Ty tyCtx ()) ->
+  uncurry (IsFunction bound a) `OnlyWhen` isFunction bound a
+reflectIsFunction [<] a = RJust (Refl, Refl)
+reflectIsFunction (bound :< (x :- ())) a with (reflectIsArrow a) | (isArrow a)
+  _ | RJust isArrow | Just (b, c) with (reflectIsFunction bound c) | (isFunction bound c)
+    _ | RJust isFunc | Just (dom, cod) = RJust (b ** c ** (isArrow , (dom ** (Refl, isFunc))))
+    _ | RNothing notFunc | _ =
+      RNothing (\(dom :< (x :- b'), cod), (b' ** c' ** (isArrow', (dom ** (Refl, isFunc)))) =>
+        let (eq1, eq2) = isArrowUnique a {b, c, d = b', e = c'} isArrow isArrow' in
+        let isFunc = rewrite eq2 in isFunc in
+        notFunc (dom, cod) isFunc)
+  _ | RNothing notArrow | _ =
+    RNothing (\(dom, cod), (b ** c ** (isArrow, _)) => notArrow (b, c) isArrow)
+
+-- Full type checking and synthesis --------------------------------------------
+
 Synths :
-  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) ->
-  SynthTerm ty tm -> Ty ty -> Type
+  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
+  SynthTerm tyCtx tmCtx -> Ty tyCtx () -> Type
 Checks :
-  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) ->
-  Ty ty -> CheckTerm ty tm -> Type
+  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Ty tyCtx () -> CheckTerm tyCtx tmCtx -> Type
 CheckSpine :
-  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) ->
-  (fun : Ty ty) -> List (CheckTerm ty tm) -> (res : Ty ty) -> Type
-CheckSpine1 :
-  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) ->
-  (fun : Ty ty) -> List1 (CheckTerm ty tm) -> (res : Ty ty) -> Type
-AllCheck : {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) -> List (Ty ty) -> List (CheckTerm ty tm) -> Type
+  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
+  (fun : Ty tyCtx ()) -> List (CheckTerm tyCtx tmCtx) -> (res : Ty tyCtx ()) -> Type
+AllCheck :
+  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Row (Ty tyCtx ()) -> Context (CheckTerm tyCtx tmCtx) -> Type
 AllCheckBinding :
-  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) -> List (Ty ty) -> Ty ty -> List (CheckTerm ty (S tm)) -> Type
-
-Synths ctx (Var i) a = (a = index i ctx)
-Synths ctx (Lit k) a = (a = TNat)
-Synths ctx (Suc t) a = (Checks ctx TNat t, a = TNat)
-Synths ctx (App e ts) a =
+  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Row (Ty tyCtx ()) -> Ty tyCtx () ->
+  Context (x : String ** CheckTerm tyCtx (tmCtx :< (x :- ()))) ->
+  Type
+
+Synths env (Var i) a = (a = indexAll i env)
+Synths env (Lit k) a = (a = TNat)
+Synths env (Suc t) a = (Checks env TNat t, a = TNat)
+Synths env (App e ts) a =
   ( fun **
-  ( Synths ctx e fun
-  , CheckSpine1 ctx fun ts a
+  ( Synths env e fun
+  , CheckSpine env fun ts a
   ))
-Synths ctx (Prj e k) a =
+Synths env (Prj e x) a =
   ( b **
-  ( Synths ctx e b
+  ( Synths env e b
   , ( as **
-    ( CanProject b as
-    , GetAt k as a
+    ( IsProduct b as
+    , GetAt x as a
     ))
   ))
-Synths ctx (Expand e) a =
+Synths env (Expand e) a =
   ( b **
-  ( Synths ctx e b
-  , ( c **
-    ( IsFixpoint b c
-    , a = sub (Base Id :< b) c))
+  ( Synths env e b
+  , ( xc **
+    ( IsFixpoint b xc
+    , a = sub (Base Id :< (fst xc :- b)) (snd xc)
+    ))
   ))
-Synths ctx (Annot t a) b =
+Synths env (Annot t a) b =
   ( Not (IllFormed a)
-  , Checks ctx a t
+  , Checks env a t
   , a = b
   )
 
-Checks ctx a (Let e t) =
+Checks env a (Let x e t) =
   ( b **
-  ( Synths ctx e b
-  , Checks (b :: ctx) a t
+  ( Synths env e b
+  , Checks (env :< (x :- b)) a t
   ))
-Checks ctx a (Abs k t) =
-  ( as : Vect (S k) _ ** b **
-  ( IsArrow (S k) a as b
-  , Checks (as ++ ctx) b t
+Checks env a (Abs bound t) =
+  ( as ** b **
+  ( IsFunction bound a as b
+  , Checks (env ++ as) b t
   ))
-Checks ctx a (Inj k t) =
+Checks env a (Inj x t) =
   ( as **
-  ( CanInject a as
+  ( IsSum a as
   , ( b **
-    ( GetAt k as b
-    , Checks ctx b t
+    ( GetAt x as b
+    , Checks env b t
     ))
   ))
-Checks ctx a (Tup ts) =
+Checks env a (Tup ts) =
   ( as **
   ( IsProduct a as
-  , AllCheck ctx as ts
+  , AllCheck env as ts
   ))
-Checks ctx a (Case e ts) =
+Checks env a (Case e ts) =
   ( b **
-  ( Synths ctx e b
+  ( Synths env e b
   , ( as **
     ( IsSum b as
-    , AllCheckBinding ctx as a ts
+    , AllCheckBinding env as a ts
     ))
   ))
-Checks ctx a (Contract t) =
-  ( b **
-  ( IsFixpoint a b
-  , Checks ctx (sub (Base Id :< a) b) t
+Checks env a (Contract t) =
+  ( xb **
+  ( IsFixpoint a xb
+  , Checks env (sub (Base Id :< (fst xb :- a)) (snd xb)) t
   ))
-Checks ctx a (Fold e t) =
+Checks env a (Fold e x t) =
   ( b **
-  ( Synths ctx e b
-  , ( c **
-    ( IsFixpoint b c
-    , Checks (sub (Base Id :< a) c :: ctx) a t
+  ( Synths env e b
+  , ( yc **
+    ( IsFixpoint b yc
+    , Checks (env :< (x :- sub (Base Id :< (fst yc :- a)) (snd yc))) a t
     ))
   ))
-Checks ctx a (Embed e) = Synths ctx e a
-
-CheckSpine ctx fun [] res = fun = res
-CheckSpine ctx fun (t :: ts) res =
-  ( a ** b **
-  ( IsArrow 1 fun [a] b
-  , Checks ctx a t
-  , CheckSpine ctx b ts res
+Checks env a (Embed e) =
+  ( b **
+  ( Synths env e b
+  , a `Eq` b
   ))
 
-CheckSpine1 ctx fun (t ::: ts) res =
+CheckSpine env fun [] res = fun = res
+CheckSpine env fun (t :: ts) res =
   ( a ** b **
-  ( IsArrow 1 fun [a] b
-  , Checks ctx a t
-  , CheckSpine ctx b ts res
+  ( IsArrow fun a b
+  , Checks env a t
+  , CheckSpine env b ts res
   ))
 
-AllCheck ctx [] [] = ()
-AllCheck ctx [] (t :: ts) = Void
-AllCheck ctx (a :: as) [] = Void
-AllCheck ctx (a :: as) (t :: ts) = (Checks ctx a t, AllCheck ctx as ts)
+AllCheck env as [<] = (as = [<])
+AllCheck env as (ts :< (x :- t)) =
+  ( a ** bs **
+  ( Remove x as a bs
+  , Checks env a t
+  , AllCheck env bs ts
+  ))
 
-AllCheckBinding ctx [] b [] = ()
-AllCheckBinding ctx [] b (t :: ts) = Void
-AllCheckBinding ctx (a :: as) b [] = Void
-AllCheckBinding ctx (a :: as) b (t :: ts) = (Checks (a :: ctx) b t, AllCheckBinding ctx as b ts)
+AllCheckBinding env as a [<] = (as = [<])
+AllCheckBinding env as a (ts :< (x :- (y ** t))) =
+  ( b ** bs **
+  ( Remove x as b bs
+  , Checks (env :< (y :- b)) a t
+  , AllCheckBinding env bs a ts
+  ))
 
--- Uniqueness
+-- Reordering
 
-getAtUnique :
-  (n : Nat) -> (xs : List a) ->
-  GetAt n xs x -> GetAt n xs y -> x = y
-getAtUnique 0     (x :: xs) (Here ** prf1)     (Here ** prf2)     = Refl
-getAtUnique (S k) (x :: xs) (There n1 ** prf1) (There n2 ** prf2) = getAtUnique k xs (n1 ** injective prf1) (n2 ** injective prf2)
-getAtUnique _     []        (n1 ** prf1)       (n2 ** prf2)       impossible
-
-canProjectUnique : (a : Ty ty) -> CanProject a as -> CanProject a bs -> as = bs
-canProjectUnique (TUnion as) Refl Refl = Refl
-canProjectUnique (TProd as)  Refl Refl = Refl
-
-canInjectUnique : (a : Ty ty) -> CanInject a as -> CanInject a bs -> as = bs
-canInjectUnique (TUnion as) Refl Refl = Refl
-canInjectUnique (TSum as)   Refl Refl = Refl
-
-isFixpointUnique : (a : Ty ty) -> IsFixpoint a b -> IsFixpoint a c -> b = c
-isFixpointUnique TNat Refl Refl = Refl
-isFixpointUnique (TFix a) Refl Refl = Refl
-
-isArrowUnique :
-  (k : Nat) -> (a : Ty ty) ->
-  forall bs, b, cs, c. IsArrow k a bs b -> IsArrow k a cs c -> (bs = cs, b = c)
-isArrowUnique 0 a (Refl, Refl) (Refl, Refl) = (Refl, Refl)
-isArrowUnique (S k) (TArrow dom cod) (as ** (Refl, prf1)) (bs ** (Refl, prf2)) =
-  let (eq1, eq2) = isArrowUnique k cod prf1 prf2 in
-  (cong (dom ::) eq1, eq2)
-
-isProductUnique : (a : Ty ty) -> IsProduct a as -> IsProduct a bs -> as = bs
-isProductUnique (TProd as) Refl Refl = Refl
+allCheckReorder :
+  as <~> bs -> (ts : Context (CheckTerm tyCtx tmCtx)) ->
+  AllCheck env as ts -> AllCheck env bs ts
+allCheckReorder [] [<] Refl = Refl
+allCheckReorder (_ :: _) [<] Refl impossible
+allCheckReorder prf (ts :< (x :- t)) (a ** bs ** (prf1, prf2, prf3)) =
+  (a ** bs ** (Evidence prf1.fst (trans (sym prf) prf1.snd), prf2, prf3))
 
-isSumUnique : (a : Ty ty) -> IsSum a as -> IsSum a bs -> as = bs
-isSumUnique (TSum as) Refl Refl = Refl
+allCheckBindingReorder :
+  as <~> bs -> (ts : Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) ->
+  AllCheckBinding env as a ts -> AllCheckBinding env bs a ts
+allCheckBindingReorder [] [<] Refl = Refl
+allCheckBindingReorder (_ :: _) [<] Refl impossible
+allCheckBindingReorder prf (ts :< (x :- (y ** t))) (b ** bs ** (prf1, prf2, prf3)) =
+  (b ** bs ** (Evidence prf1.fst (trans (sym prf) prf1.snd), prf2, prf3))
 
+-- Uniqueness
 
 synthsUnique :
-  (0 ctx : Vect tm (Ty ty)) -> (e : SynthTerm ty tm) ->
-  Synths ctx e a -> Synths ctx e b -> a = b
+  (0 env : All (const $ Ty tyCtx ()) tmCtx) -> (e : SynthTerm tyCtx tmCtx) ->
+  Synths env e a -> Synths env e b -> a = b
 checkSpineUnique :
-  (0 ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List (CheckTerm ty tm)) ->
-  CheckSpine ctx a ts b -> CheckSpine ctx a ts c -> b = c
-checkSpine1Unique :
-  (0 ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List1 (CheckTerm ty tm)) ->
-  CheckSpine1 ctx a ts b -> CheckSpine1 ctx a ts c -> b = c
-
-synthsUnique ctx (Var i) prf1 prf2 = trans prf1 (sym prf2)
-synthsUnique ctx (Lit k) prf1 prf2 = trans prf1 (sym prf2)
-synthsUnique ctx (Suc t) (_, prf1) (_, prf2) = trans prf1 (sym prf2)
-synthsUnique ctx (App e ts) (fun1 ** (prf11, prf12)) (fun2 ** (prf21, prf22))
-  with (synthsUnique ctx e prf11 prf21)
-  synthsUnique ctx (App e ts) (fun ** (prf11, prf12)) (fun ** (prf21, prf22)) | Refl =
-    checkSpine1Unique ctx fun ts prf12 prf22
-synthsUnique ctx (Prj e k) (a ** (prf11, prf12)) (b ** (prf21, prf22))
-  with (synthsUnique ctx e prf11 prf21)
-  synthsUnique ctx (Prj e k) (a ** (_, (as ** (prf11, prf12)))) (a ** (_, (bs ** (prf21, prf22)))) | Refl
-    with (canProjectUnique a prf11 prf21)
-    synthsUnique ctx (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl =
+  (0 env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (fun : Ty tyCtx ()) -> (ts : List (CheckTerm tyCtx tmCtx)) ->
+  CheckSpine env fun ts a -> CheckSpine env fun ts b -> a = b
+
+synthsUnique env (Var i) prf1 prf2 = trans prf1 (sym prf2)
+synthsUnique env (Lit k) prf1 prf2 = trans prf1 (sym prf2)
+synthsUnique env (Suc t) (_, prf1) (_, prf2) = trans prf1 (sym prf2)
+synthsUnique env (App e ts) (fun1 ** (prf11, prf12)) (fun2 ** (prf21, prf22))
+  with (synthsUnique env e prf11 prf21)
+  synthsUnique env (App e ts) (fun ** (prf11, prf12)) (fun ** (prf21, prf22)) | Refl =
+    checkSpineUnique env fun ts prf12 prf22
+synthsUnique env (Prj e k) (a ** (prf11, prf12)) (b ** (prf21, prf22))
+  with (synthsUnique env e prf11 prf21)
+  synthsUnique env (Prj e k) (a ** (_, (as ** (prf11, prf12)))) (a ** (_, (bs ** (prf21, prf22)))) | Refl
+    with (isProductUnique a prf11 prf21)
+    synthsUnique env (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl =
       getAtUnique k as prf1 prf2
-synthsUnique ctx (Expand e) (a ** (prf11, prf12)) (b ** (prf21, prf22))
-  with (synthsUnique ctx e prf11 prf21)
-  synthsUnique ctx (Expand e) (a ** (_, (b ** (prf11, prf12)))) (a ** (_, (c ** (prf21, prf22)))) | Refl
+synthsUnique env (Expand e) (a ** (prf11, prf12)) (b ** (prf21, prf22))
+  with (synthsUnique env e prf11 prf21)
+  synthsUnique env (Expand e) (a ** (_, (b ** (prf11, prf12)))) (a ** (_, (c ** (prf21, prf22)))) | Refl
     with (isFixpointUnique a prf11 prf21)
-    synthsUnique ctx (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl =
+    synthsUnique env (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl =
       trans prf1 (sym prf2)
-synthsUnique ctx (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2)
-
-checkSpineUnique ctx a [] prf1 prf2 = trans (sym prf1) prf2
-checkSpineUnique ctx a (t :: ts) (b ** c ** (prf11, _ , prf12)) (d ** e ** (prf21, _ , prf22))
-  with (isArrowUnique 1 a prf11 prf21)
-  checkSpineUnique ctx a (t :: ts) (b ** c ** (_, _ , prf1)) (b ** c ** (_, _ , prf2)) | (Refl, Refl) =
-    checkSpineUnique ctx c ts prf1 prf2
-
-checkSpine1Unique ctx a (t ::: ts) (b ** c ** (prf11, _ , prf12)) (d ** e ** (prf21, _ , prf22))
-  with (isArrowUnique 1 a prf11 prf21)
-  checkSpine1Unique ctx a (t ::: ts) (b ** c ** (_, _ , prf1)) (b ** c ** (_, _ , prf2)) | (Refl, Refl) =
-    checkSpineUnique ctx c ts prf1 prf2
-
--- Decidable -------------------------------------------------------------------
-
-canProject : Ty ty -> Maybe (List (Ty ty))
-canProject (TUnion as) = Just (forget as)
-canProject (TProd as) = Just as
-canProject _ = Nothing
-
-canInject : Ty ty -> Maybe (List (Ty ty))
-canInject (TUnion as) = Just (forget as)
-canInject (TSum as) = Just as
-canInject _ = Nothing
-
-isFixpoint : Ty ty -> Maybe (Ty (S ty))
-isFixpoint TNat = Just (TSum [TProd [], TVar FZ])
-isFixpoint (TFix a) = Just a
-isFixpoint _ = Nothing
-
-isArrow : (k : Nat) -> Ty ty -> Maybe (Vect k (Ty ty), Ty ty)
-isArrow 0 a = Just ([], a)
-isArrow (S k) (TArrow a b) = do
-  (as, c) <- isArrow k b
-  Just (a :: as, c)
-isArrow (S k) _ = Nothing
+synthsUnique env (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2)
 
-isProduct : Ty ty -> Maybe (List (Ty ty))
-isProduct (TProd as) = Just as
-isProduct _ = Nothing
+checkSpineUnique env fun [] prf1 prf2 = trans (sym prf1) prf2
+checkSpineUnique env fun (t :: ts) (a ** b ** (prf11, _ , prf12)) (c ** d ** (prf21, _ , prf22))
+  with (isArrowUnique fun prf11 prf21)
+  checkSpineUnique env fun (t :: ts) (a ** b ** (_, _ , prf1)) (a ** b ** (_, _ , prf2)) | (Refl, Refl) =
+    checkSpineUnique env b ts prf1 prf2
 
-isSum : Ty ty -> Maybe (List (Ty ty))
-isSum (TSum as) = Just as
-isSum _ = Nothing
+-- Decision
 
 synths :
-  (ctx : Vect tm (Ty ty)) ->
-  SynthTerm ty tm -> Maybe (Ty ty)
+  (env : All (const (Ty tyCtx ())) tmCtx) ->
+  SynthTerm tyCtx tmCtx -> Maybe (Ty tyCtx ())
 checks :
-  (ctx : Vect tm (Ty ty)) ->
-  Ty ty -> CheckTerm ty tm -> Bool
+  (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Ty tyCtx () -> CheckTerm tyCtx tmCtx -> Bool
 checkSpine :
-  (ctx : Vect tm (Ty ty)) ->
-  Ty ty -> List (CheckTerm ty tm) -> Maybe (Ty ty)
-checkSpine1 :
-  (ctx : Vect tm (Ty ty)) ->
-  Ty ty -> List1 (CheckTerm ty tm) -> Maybe (Ty ty)
+  (env : All (const (Ty tyCtx ())) tmCtx) ->
+  (fun : Ty tyCtx ()) -> List (CheckTerm tyCtx tmCtx) -> Maybe (Ty tyCtx ())
 allCheck :
-  (ctx : Vect tm (Ty ty)) ->
-  List (Ty ty) -> List (CheckTerm ty tm) -> Bool
+  (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Row (Ty tyCtx ()) -> Context (CheckTerm tyCtx tmCtx) -> Bool
 allCheckBinding :
-  (ctx : Vect tm (Ty ty)) ->
-  List (Ty ty) -> Ty ty -> List (CheckTerm ty (S tm)) -> Bool
-
-synths ctx (Var i) = Just (index i ctx)
-synths ctx (Lit k) = Just TNat
-synths ctx (Suc t) = do
-  guard (checks ctx TNat t)
+  (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Row (Ty tyCtx ()) -> Ty tyCtx () ->
+  Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) ->
+  Bool
+
+synths env (Var i) = Just (indexAll i env)
+synths env (Lit k) = Just TNat
+synths env (Suc t) = do
+  guard (checks env TNat t)
   Just TNat
-synths ctx (App e ts) = do
-  a <- synths ctx e
-  checkSpine1 ctx a ts
-synths ctx (Prj e k) = do
-  a <- synths ctx e
-  as <- canProject a
+synths env (App e ts) = do
+  a <- synths env e
+  checkSpine env a ts
+synths env (Prj e k) = do
+  a <- synths env e
+  as <- isProduct a
   getAt k as
-synths ctx (Expand e) = do
-  a <- synths ctx e
-  b <- isFixpoint a
-  Just (sub (Base Id :< a) b)
-synths ctx (Annot t a) = do
+synths env (Expand e) = do
+  a <- synths env e
+  (x ** b) <- isFixpoint a
+  Just (sub (Base Id :< (x :- a)) b)
+synths env (Annot t a) = do
   guard (not $ illFormed a)
-  guard (checks ctx a t)
+  guard (checks env a t)
   Just a
 
-checks ctx a (Let e t) =
-  case synths ctx e of
-    Just b => checks (b :: ctx) a t
+checks env a (Let x e t) =
+  case synths env e of
+    Just b => checks (env :< (x :- b)) a t
     Nothing => False
-checks ctx a (Abs k t) =
-  case isArrow (S k) a of
-    Just (as, b) => checks (as ++ ctx) b t
+checks env a (Abs bound t) =
+  case isFunction bound a of
+    Just (dom, cod) => checks (env ++ dom) cod t
     Nothing => False
-checks ctx a (Inj k t) =
-  case canInject a of
+checks env a (Inj k t) =
+  case isSum a of
     Just as =>
       case getAt k as of
-        Just b => checks ctx b t
+        Just b => checks env b t
         Nothing => False
     Nothing => False
-checks ctx a (Tup ts) =
+checks env a (Tup ts) =
   case isProduct a of
-    Just as => allCheck ctx as ts
+    Just as => allCheck env as ts
     Nothing => False
-checks ctx a (Case e ts) =
-  case synths ctx e of
+checks env a (Case e ts) =
+  case synths env e of
     Just b =>
       case isSum b of
-        Just as => allCheckBinding ctx as a ts
+        Just as => allCheckBinding env as a ts
         Nothing => False
     Nothing => False
-checks ctx a (Contract t) =
+checks env a (Contract t) =
   case isFixpoint a of
-    Just b => checks ctx (sub (Base Id :< a) b) t
+    Just (x ** b) => checks env (sub (Base Id :< (x :- a)) b) t
     Nothing => False
-checks ctx a (Fold e t) =
-  case synths ctx e of
+checks env a (Fold e x t) =
+  case synths env e of
     Just b =>
       case isFixpoint b of
-        Just c => checks (sub (Base Id :< a) c :: ctx) a t
+        Just (y ** c) => checks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t
         Nothing => False
     Nothing => False
-checks ctx a (Embed e) =
-  case synths ctx e of
+checks env a (Embed e) =
+  case synths env e of
     Just b => a == b
     Nothing => False
 
-checkSpine ctx a [] = Just a
-checkSpine ctx a (t :: ts) = do
-  ([dom], cod) <- isArrow 1 a
-  guard (checks ctx dom t)
-  checkSpine ctx cod ts
+checkSpine env a [] = Just a
+checkSpine env a (t :: ts) = do
+  (dom, cod) <- isArrow a
+  guard (checks env dom t)
+  checkSpine env cod ts
 
-checkSpine1 ctx a (t ::: ts) = do
-  ([dom], cod) <- isArrow 1 a
-  guard (checks ctx dom t)
-  checkSpine ctx cod ts
-
-allCheck ctx [] [] = True
-allCheck ctx [] (t :: ts) = False
-allCheck ctx (a :: as) [] = False
-allCheck ctx (a :: as) (t :: ts) = checks ctx a t && allCheck ctx as ts
+allCheck env as [<] = null as
+allCheck env as (ts :< (x :- t)) =
+  case remove' x as of
+    Just (a, bs) => checks env a t && allCheck env bs ts
+    Nothing => False
 
-allCheckBinding ctx [] b [] = True
-allCheckBinding ctx [] b (t :: ts) = False
-allCheckBinding ctx (a :: as) b [] = False
-allCheckBinding ctx (a :: as) b (t :: ts) = checks (a :: ctx) b t && allCheckBinding ctx as b ts
+allCheckBinding env as a [<] = null as
+allCheckBinding env as a (ts :< (x :- (y ** t))) =
+  case remove' x as of
+    Just (b, bs) => checks (env :< (y :- b)) a t && allCheckBinding env bs a ts
+    Nothing => False
 
 -- Proof
 
-reflectGetAt : (k : Nat) -> (xs : List a) -> GetAt k xs `OnlyWhen` getAt k xs
-reflectGetAt k [] = RNothing (\_, (n ** prf) => absurd n)
-reflectGetAt 0 (x :: xs) = RJust (Here ** Refl)
-reflectGetAt (S k) (x :: xs) with (reflectGetAt k xs) | (getAt k xs)
-  _ | RJust (n ** prf) | _ = RJust (There n ** cong S prf)
-  _ | RNothing not | _ = RNothing (\x => \case (There n ** prf) => not x (n ** injective prf))
-
-reflectCanProject : (a : Ty ty) -> CanProject a `OnlyWhen` canProject a
-reflectCanProject (TVar i) = RNothing (\x, y => y)
-reflectCanProject TNat = RNothing (\x, y => y)
-reflectCanProject (TArrow a b) = RNothing (\x, y => y)
-reflectCanProject (TUnion as) = RJust Refl
-reflectCanProject (TProd as) = RJust Refl
-reflectCanProject (TSum as) = RNothing (\x, y => y)
-reflectCanProject (TFix a) = RNothing (\x, y => y)
-
-reflectCanInject : (a : Ty ty) -> CanInject a `OnlyWhen` canInject a
-reflectCanInject (TVar i) = RNothing (\x, y => y)
-reflectCanInject TNat = RNothing (\x, y => y)
-reflectCanInject (TArrow a b) = RNothing (\x, y => y)
-reflectCanInject (TUnion as) = RJust Refl
-reflectCanInject (TProd as) = RNothing (\x, y => y)
-reflectCanInject (TSum as) = RJust Refl
-reflectCanInject (TFix a) = RNothing (\x, y => y)
-
-reflectIsFixpoint : (a : Ty ty) -> IsFixpoint a `OnlyWhen` isFixpoint a
-reflectIsFixpoint (TVar i) = RNothing (\x, y => y)
-reflectIsFixpoint TNat = RJust Refl
-reflectIsFixpoint (TArrow a b) = RNothing (\x, y => y)
-reflectIsFixpoint (TUnion as) = RNothing (\x, y => y)
-reflectIsFixpoint (TProd as) = RNothing (\x, y => y)
-reflectIsFixpoint (TSum as) = RNothing (\x, y => y)
-reflectIsFixpoint (TFix a) = RJust Refl
-
-reflectIsArrow : (k : Nat) -> (a : Ty ty) -> uncurry (IsArrow k a) `OnlyWhen` isArrow k a
-reflectIsArrow 0 a = RJust (Refl, Refl)
-reflectIsArrow (S k) (TVar i) = RNothing (\(_, _), x => x)
-reflectIsArrow (S k) TNat = RNothing (\(_, _), x => x)
-reflectIsArrow (S k) (TArrow a b) with (reflectIsArrow k b) | (isArrow k b)
-  _ | RJust arrow | Just (as, c) = RJust (as ** (Refl, arrow))
-  _ | RNothing notArrow | _ = RNothing (\(a :: as, c), (as ** (Refl, prf)) => notArrow (as, c) prf)
-reflectIsArrow (S k) (TUnion as) = RNothing (\(_, _), x => x)
-reflectIsArrow (S k) (TProd as) = RNothing (\(_, _), x => x)
-reflectIsArrow (S k) (TSum as) = RNothing (\(_, _), x => x)
-reflectIsArrow (S k) (TFix a) = RNothing (\(_, _), x => x)
-
-reflectIsProduct : (a : Ty ty) -> IsProduct a `OnlyWhen` isProduct a
-reflectIsProduct (TVar i) = RNothing (\x, y => y)
-reflectIsProduct TNat = RNothing (\x, y => y)
-reflectIsProduct (TArrow a b) = RNothing (\x, y => y)
-reflectIsProduct (TUnion as) = RNothing (\x, y => y)
-reflectIsProduct (TProd as) = RJust Refl
-reflectIsProduct (TSum as) = RNothing (\x, y => y)
-reflectIsProduct (TFix a) = RNothing (\x, y => y)
-
-reflectIsSum : (a : Ty ty) -> IsSum a `OnlyWhen` isSum a
-reflectIsSum (TVar i) = RNothing (\x, y => y)
-reflectIsSum TNat = RNothing (\x, y => y)
-reflectIsSum (TArrow a b) = RNothing (\x, y => y)
-reflectIsSum (TUnion as) = RNothing (\x, y => y)
-reflectIsSum (TProd as) = RNothing (\x, y => y)
-reflectIsSum (TSum as) = RJust Refl
-reflectIsSum (TFix a) = RNothing (\x, y => y)
-
 -- FIXME: these are total; the termination checker is unreasonably slow.
 
 partial
-reflectSynths :
-  (ctx : Vect tm (Ty ty)) -> (e : SynthTerm ty tm) ->
-  Synths ctx e `OnlyWhen` synths ctx e
-partial
-reflectChecks :
-  (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (t : CheckTerm ty tm) ->
-  Checks ctx a t `Reflects` checks ctx a t
+0 reflectSynths :
+  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (e : SynthTerm tyCtx tmCtx) ->
+  Synths env e `OnlyWhen` synths env e
 partial
-reflectCheckSpine :
-  (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List (CheckTerm ty tm)) ->
-  CheckSpine ctx a ts `OnlyWhen` checkSpine ctx a ts
+0 reflectChecks :
+  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (a : Ty tyCtx ()) -> (t : CheckTerm tyCtx tmCtx) ->
+  Checks env a t `Reflects` checks env a t
 partial
-reflectCheckSpine1 :
-  (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List1 (CheckTerm ty tm)) ->
-  CheckSpine1 ctx a ts `OnlyWhen` checkSpine1 ctx a ts
+0 reflectCheckSpine :
+  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (fun : Ty tyCtx ()) -> (ts : List (CheckTerm tyCtx tmCtx)) ->
+  CheckSpine env fun ts `OnlyWhen` checkSpine env fun ts
 partial
-reflectAllCheck :
-  (ctx : Vect tm (Ty ty)) -> (as : List (Ty ty)) -> (ts : List (CheckTerm ty tm)) ->
-  AllCheck ctx as ts `Reflects` allCheck ctx as ts
+0 reflectAllCheck :
+  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (as : Row (Ty tyCtx ())) -> (ts : Context (CheckTerm tyCtx tmCtx)) ->
+  AllCheck env as ts `Reflects` allCheck env as ts
 partial
-reflectAllCheckBinding :
-  (ctx : Vect tm (Ty ty)) -> (as : List (Ty ty)) -> (a : Ty ty) -> (ts : List (CheckTerm ty (S tm))) ->
-  AllCheckBinding ctx as a ts `Reflects` allCheckBinding ctx as a ts
-
-reflectSynths ctx (Var i) = RJust Refl
-reflectSynths ctx (Lit k) = RJust Refl
-reflectSynths ctx (Suc t) with (reflectChecks ctx TNat t) | (checks ctx TNat t)
+0 reflectAllCheckBinding :
+  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (as : Row (Ty tyCtx ())) -> (a : Ty tyCtx ()) ->
+  (ts : Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) ->
+  AllCheckBinding env as a ts `Reflects` allCheckBinding env as a ts
+
+reflectSynths env (Var i) = RJust Refl
+reflectSynths env (Lit k) = RJust Refl
+reflectSynths env (Suc t) with (reflectChecks env TNat t) | (checks env TNat t)
   _ | RTrue tNat | _ = RJust (tNat, Refl)
   _ | RFalse tNotNat | _ = RNothing (\_, (tNat, _) => tNotNat tNat)
-reflectSynths ctx (App e ts) with (reflectSynths ctx e) | (synths ctx e)
-  _ | RJust eTy | Just a with (reflectCheckSpine1 ctx a ts) | (checkSpine1 ctx a ts)
+reflectSynths env (App e ts) with (reflectSynths env e) | (synths env e)
+  _ | RJust eTy | Just a with (reflectCheckSpine env a ts) | (checkSpine env a ts)
     _ | RJust tsSpine | Just b = RJust (a ** (eTy, tsSpine))
     _ | RNothing tsBad | _ =
       RNothing
         (\c, (b ** (eTy', tsSpine)) =>
-          let tsSpine = rewrite synthsUnique ctx e {a, b} eTy eTy' in tsSpine in
+          let tsSpine = rewrite synthsUnique env e {a, b} eTy eTy' in tsSpine in
           tsBad c tsSpine)
   _ | RNothing eBad | _ =
     RNothing (\c, (b ** (eTy, _)) => eBad b eTy)
-reflectSynths ctx (Prj e k) with (reflectSynths ctx e) | (synths ctx e)
-  _ | RJust eTy | Just a with (reflectCanProject a) | (canProject a)
-    _ | RJust prf | Just as with (reflectGetAt k as) | (getAt k as)
+reflectSynths env (Prj e x) with (reflectSynths env e) | (synths env e)
+  _ | RJust eTy | Just a with (reflectIsProduct a) | (isProduct a)
+    _ | RJust prf | Just as with (reflectGetAt x as) | (getAt x as)
       _ | RJust got | Just b = RJust (a ** (eTy, (as ** (prf, got))))
       _ | RNothing not | _ =
         RNothing (\x, (a' ** (eTy', (as' ** (prf', got)))) =>
-          let prf' = rewrite synthsUnique ctx e {a, b = a'} eTy eTy' in prf' in
-          let got = rewrite canProjectUnique a {as, bs = as'} prf prf' in got in
+          let prf' = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf' in
+          let got = rewrite isProductUnique a {as, bs = as'} prf prf' in got in
           not x got)
     _ | RNothing nprf | _ =
       RNothing (\x, (a' ** (eTy', (as' ** (prf, _)))) =>
-        let prf = rewrite synthsUnique ctx e {a, b = a'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf in
         nprf as' prf)
   _ | RNothing eBad | _ = RNothing (\x, (a' ** (eTy, _)) => eBad a' eTy)
-reflectSynths ctx (Expand e) with (reflectSynths ctx e) | (synths ctx e)
+reflectSynths env (Expand e) with (reflectSynths env e) | (synths env e)
   _ | RJust eTy | Just a with (reflectIsFixpoint a) | (isFixpoint a)
-    _ | RJust prf | Just b = RJust (a ** (eTy, (b ** (prf, Refl))))
+    _ | RJust prf | Just (x ** b) = RJust (a ** (eTy, ((x ** b) ** (prf, Refl))))
     _ | RNothing nprf | _ =
       RNothing (\x, (a' ** (eTy', (b ** (prf, eq)))) =>
-        let prf = rewrite synthsUnique ctx e {a, b = a'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf in
         nprf b prf)
   _ | RNothing eBad | _ = RNothing (\x, (a ** (eTy, _)) => eBad a eTy)
-reflectSynths ctx (Annot t a) with (reflectIllFormed a) | (illFormed a)
-  _ | RFalse wf | _ with (reflectChecks ctx a t) | (checks ctx a t)
+reflectSynths env (Annot t a) with (reflectIllFormed a) | (illFormed a)
+  _ | RFalse wf | _ with (reflectChecks env a t) | (checks env a t)
     _ | RTrue tTy | _ = RJust (wf, tTy, Refl)
     _ | RFalse tBad | _ = RNothing (\x, (_, tTy, Refl) => tBad tTy)
   _ | RTrue notWf | _ = RNothing (\x, (wf, _) => wf notWf)
 
-reflectChecks ctx a (Let e t) with (reflectSynths ctx e) | (synths ctx e)
-  _ | RJust eTy | Just b with (reflectChecks (b :: ctx) a t) | (checks (b :: ctx) a t)
+reflectChecks env a (Let x e t) with (reflectSynths env e) | (synths env e)
+  _ | RJust eTy | Just b with (reflectChecks (env :< (x :- b)) a t) | (checks (env :< (x :- b)) a t)
     _ | RTrue tTy | _ = RTrue (b ** (eTy, tTy))
     _ | RFalse tBad | _ =
       RFalse (\(b' ** (eTy', tTy)) =>
-        let tTy = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in tTy in
+        let tTy = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in tTy in
         tBad tTy)
   _ | RNothing eBad | Nothing = RFalse (\(b ** (eTy, _)) => eBad b eTy)
-reflectChecks ctx a (Abs k t) with (reflectIsArrow (S k) a) | (isArrow (S k) a)
-  _ | RJust prf | Just (as, b) with (reflectChecks (as ++ ctx) b t) | (checks (as ++ ctx) b t)
+reflectChecks env a (Abs bound t) with (reflectIsFunction bound a) | (isFunction bound a)
+  _ | RJust prf | Just (as, b) with (reflectChecks (env ++ as) b t) | (checks (env ++ as) b t)
     _ | RTrue tTy | _ = RTrue (as ** b ** (prf, tTy))
     _ | RFalse tBad | _ =
       RFalse (\(as' ** b' ** (prf', tTy)) =>
         let
-          tTy =
-            rewrite fst $ isArrowUnique (S k) a {bs = as, b, cs = as', c = b'} prf prf' in
-            rewrite snd $ isArrowUnique (S k) a {bs = as, b, cs = as', c = b'} prf prf' in
-            tTy
+          (eq1, eq2) =
+            isFunctionUnique bound a
+              {dom1 = as, cod1 = b, dom2 = as', cod2 = b'}
+              prf prf'
+          tTy = rewrite eq1 in rewrite eq2 in tTy
         in
         tBad tTy)
   _ | RNothing nprf | _ = RFalse (\(as ** b ** (prf, _)) => nprf (as, b) prf)
-reflectChecks ctx a (Inj k t) with (reflectCanInject a) | (canInject a)
+reflectChecks env a (Inj k t) with (reflectIsSum a) | (isSum a)
   _ | RJust prf | Just as with (reflectGetAt k as) | (getAt k as)
-    _ | RJust got | Just b with (reflectChecks ctx b t) | (checks ctx b t)
+    _ | RJust got | Just b with (reflectChecks env b t) | (checks env b t)
       _ | RTrue tTy | _ = RTrue (as ** (prf, (b ** (got, tTy))))
       _ | RFalse tBad | _ =
         RFalse (\(as' ** (prf', (b' ** (got', tTy)))) =>
-          let got' = rewrite canInjectUnique a {as, bs = as'} prf prf' in got' in
-          let tTy = rewrite getAtUnique k as {x = b, y = b'} got got' in tTy in
-          tBad tTy)
+          let got' = rewrite isSumUnique a {as, bs = as'} prf prf' in got' in
+          let tTy = rewrite getAtUnique k as {y = b, z = b'} got got' in tTy in
+          tBad tTy
+          )
     _ | RNothing not | _ =
       RFalse (\(as' ** (prf', (b ** (got, _)))) =>
-        let got = rewrite canInjectUnique a {as, bs = as'} prf prf' in got in
+        let got = rewrite isSumUnique a {as, bs = as'} prf prf' in got in
         not b got)
   _ | RNothing nprf | _ = RFalse (\(as ** (prf, _)) => nprf as prf)
-reflectChecks ctx a (Tup ts) with (reflectIsProduct a) | (isProduct a)
-  _ | RJust prf | Just as with (reflectAllCheck ctx as ts) | (allCheck ctx as ts)
+reflectChecks env a (Tup ts) with (reflectIsProduct a) | (isProduct a)
+  _ | RJust prf | Just as with (reflectAllCheck env as ts) | (allCheck env as ts)
     _ | RTrue tsTy | _ = RTrue (as ** (prf, tsTy))
     _ | RFalse tsBad | _ =
       RFalse (\(as' ** (prf', tsTy)) =>
         let tsTy = rewrite isProductUnique a {as, bs = as'} prf prf' in tsTy in
         tsBad tsTy)
   _ | RNothing nprf | _ = RFalse (\(as ** (prf, _)) => nprf as prf)
-reflectChecks ctx a (Case e ts) with (reflectSynths ctx e) | (synths ctx e)
+reflectChecks env a (Case e ts) with (reflectSynths env e) | (synths env e)
   _ | RJust eTy | Just b with (reflectIsSum b) | (isSum b)
-    _ | RJust prf | Just as with (reflectAllCheckBinding ctx as a ts) | (allCheckBinding ctx as a ts)
+    _ | RJust prf | Just as with (reflectAllCheckBinding env as a ts) | (allCheckBinding env as a ts)
       _ | RTrue tsTy | _ = RTrue (b ** (eTy, (as ** (prf, tsTy))))
       _ | RFalse tsBad | _ =
         RFalse
           (\(b' ** (eTy', (as' ** (prf', tsTy)))) =>
-            let prf' = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf' in
+            let prf' = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf' in
             let tsTy = rewrite isSumUnique b {as, bs = as'} prf prf' in tsTy in
             tsBad tsTy)
     _ | RNothing nprf | _ =
       RFalse (\(b' ** (eTy', (as ** (prf, _)))) =>
-        let prf = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf in
         nprf as prf)
   _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy)
-reflectChecks ctx a (Contract t) with (reflectIsFixpoint a) | (isFixpoint a)
-  _ | RJust prf | Just b with (reflectChecks ctx (sub (Base Id :< a) b) t) | (checks ctx (sub (Base Id :< a) b) t)
-    _ | RTrue tTy | _ = RTrue (b ** (prf, tTy))
+reflectChecks env a (Contract t) with (reflectIsFixpoint a) | (isFixpoint a)
+  _ | RJust prf | Just (x ** b) with (reflectChecks env (sub (Base Id :< (x :- a)) b) t) | (checks env (sub (Base Id :< (x :- a)) b) t)
+    _ | RTrue tTy | _ = RTrue ((x ** b) ** (prf, tTy))
     _ | RFalse tBad | _ =
       RFalse (\(b' ** (prf', tTy)) =>
-        let tTy = rewrite isFixpointUnique a {b, c = b'} prf prf' in tTy in
+        let
+          eq = isFixpointUnique a {xb = (x ** b), yc = b'} prf prf'
+          tTy =
+            replace {p = \xb => Checks env (sub (Base Id :< (xb.fst :- a)) xb.snd) t}
+              (sym eq) tTy
+        in
         tBad tTy)
   _ | RNothing nprf | _ = RFalse (\(b ** (prf, _)) => nprf b prf)
-reflectChecks ctx a (Fold e t) with (reflectSynths ctx e) | (synths ctx e)
+reflectChecks env a (Fold e x t) with (reflectSynths env e) | (synths env e)
   _ | RJust eTy | Just b with (reflectIsFixpoint b) | (isFixpoint b)
-    _ | RJust prf | Just c with (reflectChecks ((sub (Base Id :< a) c) :: ctx) a t) | (checks ((sub (Base Id :< a) c) :: ctx) a t)
-      _ | RTrue tTy | _ = RTrue (b ** (eTy, (c ** (prf, tTy))))
+    _ | RJust prf | Just (y ** c) with (reflectChecks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t) | (checks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t)
+      _ | RTrue tTy | _ = RTrue (b ** (eTy, ((y ** c) ** (prf, tTy))))
       _ | RFalse tBad | _ =
         RFalse (\(b' ** (eTy', (c' ** (prf', tTy)))) =>
-          let prf' = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf' in
-          let tTy = rewrite isFixpointUnique b {b = c, c = c'} prf prf' in tTy in
+          let
+            prf' = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf'
+            eq = isFixpointUnique b {xb = (y ** c), yc = c'} prf prf'
+            tTy =
+              replace {p = \yc => Checks (env :< (x :- sub (Base Id :< (yc.fst :- a)) yc.snd)) a t}
+                (sym eq) tTy
+          in
           tBad tTy)
     _ | RNothing nprf | _ =
       RFalse (\(b' ** (eTy', (c ** (prf, _)))) =>
-        let prf = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf in
         nprf c prf)
   _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy)
-reflectChecks ctx a (Embed e) with (reflectSynths ctx e) | (synths ctx e)
+reflectChecks env a (Embed e) with (reflectSynths env e) | (synths env e)
   _ | RJust eTy | Just b with (reflectEq a b) | (a == b)
-    reflectChecks ctx a (Embed e) | RJust eTy | Just .(a) | RTrue Refl | _ = RTrue eTy
-    _ | RFalse neq | _ = RFalse (\eTy' => neq $ synthsUnique ctx e eTy' eTy)
-  _ | RNothing eBad | _ = RFalse (\eTy => eBad a eTy)
-
-reflectCheckSpine ctx a [] = RJust Refl
-reflectCheckSpine ctx a (t :: ts) with (reflectIsArrow 1 a) | (isArrow 1 a)
-  _ | RJust prf | Just ([b], c) with (reflectChecks ctx b t) | (checks ctx b t)
-    _ | RTrue tTy | _ with (reflectCheckSpine ctx c ts) | (checkSpine ctx c ts)
-      _ | RJust tsTy | Just d = RJust (b ** c ** (prf, tTy, tsTy))
-      _ | RNothing tsBad | _ =
-        RNothing (\d, (_ ** c' ** (prf', _, tsTy)) =>
-          let tsTy = rewrite snd $ isArrowUnique 1 a {b = c, c = c'} prf prf' in tsTy in
-          tsBad d tsTy)
-    _ | RFalse tBad | _ =
-      RNothing (\d, (b' ** _ ** (prf', tTy, _)) =>
-        let
-          tTy =
-            rewrite fst $ biinj (::) $ fst $ isArrowUnique 1 a {bs = [b], cs = [b']} prf prf' in
-            tTy
-        in
-        tBad tTy)
-  _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf ([b], c) prf)
+    _ | RTrue eq | _ = RTrue (b ** (eTy, eq))
+    _ | RFalse neq | _ =
+      RFalse (\(b' ** (eTy', eq)) =>
+        let eq = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in eq in
+        neq eq)
+  _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy)
 
-reflectCheckSpine1 ctx a (t ::: ts) with (reflectIsArrow 1 a) | (isArrow 1 a)
-  _ | RJust prf | Just ([b], c) with (reflectChecks ctx b t) | (checks ctx b t)
-    _ | RTrue tTy | _ with (reflectCheckSpine ctx c ts) | (checkSpine ctx c ts)
+reflectCheckSpine env a [] = RJust Refl
+reflectCheckSpine env a (t :: ts) with (reflectIsArrow a) | (isArrow a)
+  _ | RJust prf | Just (b, c) with (reflectChecks env b t) | (checks env b t)
+    _ | RTrue tTy | _ with (reflectCheckSpine env c ts) | (checkSpine env c ts)
       _ | RJust tsTy | Just d = RJust (b ** c ** (prf, tTy, tsTy))
       _ | RNothing tsBad | _ =
         RNothing (\d, (_ ** c' ** (prf', _, tsTy)) =>
-          let tsTy = rewrite snd $ isArrowUnique 1 a {b = c, c = c'} prf prf' in tsTy in
+          let (eq1, eq2) = isArrowUnique a {c, e = c'} prf prf' in
+          let tsTy = rewrite eq2 in tsTy in
           tsBad d tsTy)
     _ | RFalse tBad | _ =
       RNothing (\d, (b' ** _ ** (prf', tTy, _)) =>
-        let
-          tTy =
-            rewrite fst $ biinj (::) $ fst $ isArrowUnique 1 a {bs = [b], cs = [b']} prf prf' in
-            tTy
-        in
+        let (eq1, eq2) = isArrowUnique a {b, d = b'} prf prf' in
+        let tTy = rewrite eq1 in tTy in
         tBad tTy)
-  _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf ([b], c) prf)
-
-reflectAllCheck ctx [] [] = RTrue ()
-reflectAllCheck ctx [] (t :: ts) = RFalse (\x => x)
-reflectAllCheck ctx (a :: as) [] = RFalse (\x => x)
-reflectAllCheck ctx (a :: as) (t :: ts) with (reflectChecks ctx a t) | (checks ctx a t)
-  _ | RTrue tTy | _ with (reflectAllCheck ctx as ts) | (allCheck ctx as ts)
-    _ | RTrue tsTy | _ = RTrue (tTy, tsTy)
-    _ | RFalse tsBad | _ = RFalse (\(_, tsTy) => tsBad tsTy)
-  _ | RFalse tBad | _ = RFalse (\(tTy, _) => tBad tTy)
-
-reflectAllCheckBinding ctx [] b [] = RTrue ()
-reflectAllCheckBinding ctx [] b (t :: ts) = RFalse (\x => x)
-reflectAllCheckBinding ctx (a :: as) b [] = RFalse (\x => x)
-reflectAllCheckBinding ctx (a :: as) b (t :: ts) with (reflectChecks (a :: ctx) b t) | (checks (a :: ctx) b t)
-  _ | RTrue tTy | _ with (reflectAllCheckBinding ctx as b ts) | (allCheckBinding ctx as b ts)
-    _ | RTrue tsTy | _ = RTrue (tTy, tsTy)
-    _ | RFalse tsBad | _ = RFalse (\(_, tsTy) => tsBad tsTy)
-  _ | RFalse tBad | _ = RFalse (\(tTy, _) => tBad tTy)
+  _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf (b, c) prf)
+
+reflectAllCheck env [<] [<] = RTrue Refl
+reflectAllCheck env (_ :< _) [<] = RFalse (\case Refl impossible)
+reflectAllCheck env as (ts :< (x :- t)) with (reflectRemove x as) | (remove' x as)
+  _ | RJust prf | Just (a, bs) with (reflectAnd (reflectChecks env a t) (reflectAllCheck env bs ts)) | (checks env a t && allCheck env bs ts)
+    _ | RTrue checks | _ = RTrue (a ** bs ** (prf, checks))
+    _ | RFalse notChecks | _ =
+      RFalse (\(a' ** bs' ** (prf', checks)) =>
+        let (eq, reorder) = removeUnique x as prf prf' in
+        notChecks $
+        bimap (\x => rewrite eq in x) (allCheckReorder (sym reorder) ts) checks)
+  _ | RNothing nprf | _ = RFalse (\(a ** bs ** (prf, _)) => nprf (a, bs) prf)
+
+reflectAllCheckBinding env [<] a [<] = RTrue Refl
+reflectAllCheckBinding env (_ :< _) a [<] = RFalse (\case Refl impossible)
+reflectAllCheckBinding env as a (ts :< (x :- (y ** t))) with (reflectRemove x as) | (remove' x as)
+  _ | RJust prf | Just (b, bs) with (reflectAnd (reflectChecks (env :< (y :- b)) a t) (reflectAllCheckBinding env bs a ts)) | (checks (env :< (y :- b)) a t && allCheckBinding env bs a ts)
+    _ | RTrue checks | _ = RTrue (b ** bs ** (prf, checks))
+    _ | RFalse notChecks | _ =
+      RFalse (\(b' ** bs' ** (prf', checks)) =>
+        let (eq, reorder) = removeUnique x as prf prf' in
+        notChecks $
+        bimap (\x => rewrite eq in x) (allCheckBindingReorder (sym reorder) ts) checks)
+  _ | RNothing nprf | _ = RFalse (\(b ** bs ** (prf, _)) => nprf (b, bs) prf)
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index e353e50..71028ba 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -1,24 +1,10 @@
 module Inky.Term.Pretty
 
-import Data.Fin
-import Data.Fin.Extra
-import Data.List
-import Data.String
+import Inky.Context
 import Inky.Term
 import Inky.Type.Pretty
 import Text.PrettyPrint.Prettyprinter
 
-asTmChar : Fin 9 -> Char
-asTmChar = index' ['x', 'y', 'z', 'a', 'b', 'c', 'd', 'e', 'f']
-
-export
-termName : Nat -> String
-termName n with (divMod n 9)
-  termName _ | Fraction _ 9 q r Refl =
-    strSnoc
-      (if q == 0 then "" else assert_total (termName $ pred q))
-      (asTmChar r)
-
 appPrec, prjPrec, expandPrec, annotPrec,
   letPrec, absPrec, injPrec, tupPrec, casePrec, contractPrec, foldPrec : Prec
 appPrec = App
@@ -27,29 +13,40 @@ expandPrec = PrefixMinus
 annotPrec = Equal
 letPrec = Open
 absPrec = Open
-injPrec = User 8
-tupPrec = User 2
+injPrec = App
+tupPrec = Open
 casePrec = Open
 contractPrec = PrefixMinus
 foldPrec = Open
 
 export
-prettySynth : {ty, tm : Nat} -> SynthTerm ty tm -> Prec -> Doc ann
-prettyCheck : {ty, tm : Nat} -> CheckTerm ty tm -> Prec -> Doc ann
-prettyAllCheck : {ty, tm : Nat} -> List (CheckTerm ty tm) -> Prec -> List (Doc ann)
-prettyAll1Check : {ty, tm : Nat} -> List1 (CheckTerm ty tm) -> Prec -> List (Doc ann)
+prettySynth :
+  {tyCtx, tmCtx : Context ()} ->
+  SynthTerm tyCtx tmCtx -> Prec -> Doc ann
+prettyCheck :
+  {tyCtx, tmCtx : Context ()} ->
+  CheckTerm tyCtx tmCtx -> Prec -> Doc ann
+prettyAllCheck :
+  {tyCtx, tmCtx : Context ()} ->
+  List (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann)
+prettyCheckCtx :
+  {tyCtx, tmCtx : Context ()} ->
+  Context (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann)
+prettyCheckCtxBinding :
+  {tyCtx, tmCtx : Context ()} ->
+  Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> Prec -> List (Doc ann)
 
-prettySynth (Var i) d = pretty (termName $ finToNat i)
+prettySynth (Var i) d = pretty (unVal $ nameOf i)
 prettySynth (Lit k) d = pretty k
 prettySynth (Suc t) d =
   parenthesise (d >= appPrec) $ group $ align $ hang 2 $
     "suc" <+> line <+> prettyCheck t appPrec
 prettySynth (App e ts) d =
   parenthesise (d >= appPrec) $ group $ align $ hang 2 $
-    concatWith (\x, y => x <+> line <+> y) (prettySynth e appPrec :: prettyAll1Check ts appPrec)
-prettySynth (Prj e k) d =
+    concatWith (surround line) (prettySynth e appPrec :: prettyAllCheck ts appPrec)
+prettySynth (Prj e x) d =
   parenthesise (d > prjPrec) $ group $ align $ hang 2 $
-    prettySynth e prjPrec <+> "[" <+> line' <+> pretty k <+> line' <+> "]"
+    prettySynth e prjPrec <+> "." <+> pretty x
 prettySynth (Expand e) d =
   "!" <+>
   (parenthesise (d > expandPrec) $ group $ align $ hang 2 $
@@ -58,54 +55,56 @@ prettySynth (Annot t a) d =
   parenthesise (d > annotPrec) $ group $ align $ hang 2 $
     prettyCheck t annotPrec <++> ":" <+> line <+> prettyType a annotPrec
 
-prettyCheck (Let e t) d =
+prettyCheck (Let x e t) d =
   parenthesise (d > letPrec) $ group $ align $ hang 2 $
     "let" <++>
     (group $ align $ hang 2 $
-      pretty (termName tm) <++> "=" <+> line <+> prettySynth e letPrec
+      pretty x <++> "=" <+> line <+> prettySynth e letPrec
     ) <++>
     "in" <+> line <+>
     prettyCheck t letPrec
-prettyCheck (Abs k t) d =
+prettyCheck (Abs bound t) d =
   parenthesise (d > absPrec) $ group $ align $ hang 2 $
-    "\\" <+> concatWith (\x, y => x <+> "," <++> y) (bindings tm (S k)) <++> "=>" <+> line <+>
+    "\\" <+> concatWith (surround ",") (bindings bound <>> []) <++> "=>" <+> line <+>
     prettyCheck t absPrec
   where
-  bindings : Nat -> Nat -> List (Doc ann)
-  bindings tm 0 = []
-  bindings tm (S k) = pretty (termName tm) :: bindings (S tm) k
+  bindings : Context () -> SnocList (Doc ann)
+  bindings [<] = [<]
+  bindings (bound :< (x :- ())) = bindings bound :< pretty x
 prettyCheck (Inj k t) d =
   parenthesise (d > injPrec) $ group $ align $ hang 2 $
     "<" <+> line' <+> pretty k <+> line' <+> ">" <+> prettyCheck t injPrec
-prettyCheck (Tup []) d = pretty "()"
-prettyCheck (Tup [t]) d =
-  parens $ group $ align $ hang 2 $
-    prettyCheck t tupPrec <+> line <+> ","
 prettyCheck (Tup ts) d =
-  parenthesise (d > tupPrec) $ group $ align $ hang 2 $
-    concatWith (\x, y => x <+> "," <++> line <+> y) (prettyAllCheck ts tupPrec)
+  parens $ group $ align $ hang 2 $
+    concatWith (surround $ "," <+> line) (prettyCheckCtx ts tupPrec)
 prettyCheck (Case e ts) d =
   parenthesise (d > casePrec) $ group $ align $ hang 2 $
     "case" <++> prettySynth e casePrec <++> "of" <+> line <+>
     (braces $ align $ hang 2 $
-      concatWith (\x, y => x <+> hardline <+> y) $
-      map (\x =>
-        parens $ group $ align $ hang 2 $
-          "\\" <+> pretty (termName tm) <++> "=>" <+> line <+> x) $
-      prettyAllCheck ts casePrec
-    )
+      concatWith (surround hardline) $
+      map parens $
+      prettyCheckCtxBinding ts casePrec)
 prettyCheck (Contract t) d =
   "~" <+>
   (parenthesise (d > contractPrec) $ group $ align $ hang 2 $
     prettyCheck t contractPrec)
-prettyCheck (Fold e t) d =
+prettyCheck (Fold e x t) d =
   parenthesise (d > foldPrec) $ group $ align $ hang 2 $
     "fold" <++> prettySynth e foldPrec <++> "by" <+> line <+>
     (parens $ group $ align $ hang 2 $
-      "\\" <+> pretty (termName tm) <++> "=>" <+> line <+> prettyCheck t foldPrec)
+      "\\" <+> pretty x <++> "=>" <+> line <+> prettyCheck t foldPrec)
 prettyCheck (Embed e) d = prettySynth e d
 
 prettyAllCheck [] d = []
 prettyAllCheck (t :: ts) d = prettyCheck t d :: prettyAllCheck ts d
 
-prettyAll1Check (t ::: ts) d = prettyCheck t d :: prettyAllCheck ts d
+prettyCheckCtx [<] d = []
+prettyCheckCtx (ts :< (x :- t)) d =
+  (group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyCheck t d) ::
+  prettyCheckCtx ts d
+
+prettyCheckCtxBinding [<] d = []
+prettyCheckCtxBinding (ts :< (x :- (y ** t))) d =
+  (group $ align $ hang 2 $
+    "\\" <+> pretty x <++> pretty y <++> "=>" <+> line <+> prettyCheck t d) ::
+  prettyCheckCtxBinding ts d
diff --git a/src/Inky/Thinning.idr b/src/Inky/Thinning.idr
index c3235c0..3d593ae 100644
--- a/src/Inky/Thinning.idr
+++ b/src/Inky/Thinning.idr
@@ -1,7 +1,9 @@
 module Inky.Thinning
 
-import public Data.Fin
+import public Inky.Context
 
+import Data.DPair
+import Data.Nat
 import Control.Function
 
 --------------------------------------------------------------------------------
@@ -9,24 +11,27 @@ import Control.Function
 --------------------------------------------------------------------------------
 
 public export
-data Thins : Nat -> Nat -> Type where
-  Id : n `Thins` n
-  Drop : k `Thins` n -> k `Thins` S n
-  Keep : k `Thins` n -> S k `Thins` S n
+data Thins : Context a -> Context a -> Type where
+  Id : ctx `Thins` ctx
+  Drop : ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx2 :< x
+  Keep : ctx1 `Thins` ctx2 -> ctx1 :< (x :- v) `Thins` ctx2 :< (y :- v)
 
 %name Thins f, g, h
 
 -- Basics
 
+indexPos : (f : ctx1 `Thins` ctx2) -> (pos : VarPos ctx1 x v) -> Var ctx2 v
+indexPos Id pos = toVar pos
+indexPos (Drop f) pos = ThereVar (indexPos f pos)
+indexPos (Keep f) Here = toVar Here
+indexPos (Keep f) (There pos) = ThereVar (indexPos f pos)
+
 export
-index : k `Thins` n -> Fin k -> Fin n
-index Id x = x
-index (Drop f) x = FS (index f x)
-index (Keep f) FZ = FZ
-index (Keep f) (FS x) = FS (index f x)
+index : ctx1 `Thins` ctx2 -> Var ctx1 v -> Var ctx2 v
+index f i = indexPos f i.pos
 
 export
-(.) : k `Thins` n -> j `Thins` k -> j `Thins` n
+(.) : ctx2 `Thins` ctx3 -> ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx3
 Id . g = g
 Drop f . g = Drop (f . g)
 Keep f . Id = Keep f
@@ -35,43 +40,53 @@ Keep f . Keep g = Keep (f . g)
 
 -- Basic properties
 
-export
-indexInjective : (f : k `Thins` n) -> {x, y : Fin k} -> index f x = index f y -> x = y
-indexInjective Id eq = eq
-indexInjective (Drop f) eq = indexInjective f $ injective eq
-indexInjective (Keep f) {x = FZ} {y = FZ} eq = Refl
-indexInjective (Keep f) {x = FS x} {y = FS y} eq = cong FS $ indexInjective f $ injective eq
+indexPosInjective :
+  (f : ctx1 `Thins` ctx2) -> {i : VarPos ctx1 x v} -> {j : VarPos ctx1 y v} ->
+  (0 _ : toNat (indexPos f i).pos = toNat (indexPos f j).pos) -> 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
-(f : k `Thins` n) => Injective (index f) where
-  injective = indexInjective f
+indexInjective : (f : ctx1 `Thins` ctx2) -> {i, j : Var ctx1 v} -> index f i = index f j -> i = j
+indexInjective f {i = %% x, j = %% y} prf = toVarCong (indexPosInjective f $ toNatCong' prf)
 
 export
-indexId : (0 x : Fin n) -> index Id x = x
-indexId x = Refl
+indexId : (0 i : Var ctx v) -> index Id i = i
+indexId (%% x) = Refl
 
 export
-indexDrop : (0 f : k `Thins` n) -> (0 x : Fin k) -> index (Drop f) x = FS (index f x)
-indexDrop f x = Refl
+indexDrop : (0 f : ctx1 `Thins` ctx2) -> (0 i : Var ctx1 v) -> index (Drop f) i = ThereVar (index f i)
+indexDrop f (%% x) = Refl
 
 export
-indexKeepFZ : (0 f : k `Thins` n) -> index (Keep f) FZ = FZ
-indexKeepFZ f = Refl
+indexKeepHere : (0 f : ctx1 `Thins` ctx2) -> index (Keep {x, y} f) (%% x) = (%% y)
+indexKeepHere f = Refl
 
 export
-indexKeepFS : (0 f : k `Thins` n) -> (0 x : Fin k) -> index (Keep f) (FS x) = FS (index f x)
-indexKeepFS f x = Refl
+indexKeepThere :
+  (0 f : ctx1 `Thins` ctx2) -> (0 i : Var ctx1 v) ->
+  index (Keep f) (ThereVar i) = ThereVar (index f i)
+indexKeepThere f (%% x) = Refl
+
+indexPosComp :
+  (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (pos : VarPos ctx1 x v) ->
+  indexPos (f . g) pos = index f (indexPos g pos)
+indexPosComp Id g pos with (indexPos g pos)
+  _ | (%% _) = Refl
+indexPosComp (Drop f) g pos = cong ThereVar (indexPosComp f g pos)
+indexPosComp (Keep f) Id pos = Refl
+indexPosComp (Keep f) (Drop g) pos = cong ThereVar (indexPosComp f g pos)
+indexPosComp (Keep f) (Keep g) Here = Refl
+indexPosComp (Keep f) (Keep g) (There pos) = cong ThereVar (indexPosComp f g pos)
 
 export
 indexComp :
-  (f : k `Thins` n) -> (g : j `Thins` k) -> (x : Fin j) ->
-  index (f . g) x = index f (index g x)
-indexComp Id g x = Refl
-indexComp (Drop f) g x = cong FS (indexComp f g x)
-indexComp (Keep f) Id x = Refl
-indexComp (Keep f) (Drop g) x = cong FS (indexComp f g x)
-indexComp (Keep f) (Keep g) FZ = Refl
-indexComp (Keep f) (Keep g) (FS x) = cong FS (indexComp f g x)
+  (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (i : Var ctx1 v) ->
+  index (f . g) i = index f (index g i)
+indexComp f g i = indexPosComp f g i.pos
 
 -- Congruence ------------------------------------------------------------------
 
@@ -79,7 +94,7 @@ export
 infix 6 ~~~
 
 public export
-data (~~~) : k `Thins` n -> k `Thins` n -> Type where
+data (~~~) : ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx2 -> Type where
   IdId : Id ~~~ Id
   IdKeep : Id ~~~ f -> Id ~~~ Keep f
   KeepId : f ~~~ Id -> Keep f ~~~ Id
@@ -88,86 +103,95 @@ data (~~~) : k `Thins` n -> k `Thins` n -> Type where
 
 %name Thinning.(~~~) prf
 
-export
-(.index) : f ~~~ g -> (x : Fin k) -> index f x = index g x
-(IdId).index x = Refl
-(IdKeep prf).index FZ = Refl
-(IdKeep prf).index (FS x) = cong FS (prf.index x)
-(KeepId prf).index FZ = Refl
-(KeepId prf).index (FS x) = cong FS (prf.index x)
-(DropDrop prf).index x = cong FS (prf.index x)
-(KeepKeep prf).index FZ = Refl
-(KeepKeep prf).index (FS x) = cong FS (prf.index x)
+(.indexPos) : f ~~~ g -> (pos : VarPos ctx1 x v) -> indexPos f pos = indexPos g pos
+(IdId).indexPos pos = Refl
+(IdKeep prf).indexPos Here = Refl
+(IdKeep prf).indexPos (There pos) = cong ThereVar $ prf.indexPos pos
+(KeepId prf).indexPos Here = Refl
+(KeepId prf).indexPos (There pos) = cong ThereVar $ prf.indexPos pos
+(DropDrop prf).indexPos pos = cong ThereVar $ prf.indexPos pos
+(KeepKeep prf).indexPos Here = Refl
+(KeepKeep prf).indexPos (There pos) = cong ThereVar $ prf.indexPos pos
 
 export
-pointwise : {f, g : k `Thins` n} -> (0 _ : (x : Fin k) -> index f x = index g x) -> f ~~~ g
-pointwise {f = Id} {g = Id} prf = IdId
-pointwise {f = Id} {g = Drop g} prf = void $ absurd $ prf FZ
-pointwise {f = Id} {g = Keep g} prf = IdKeep (pointwise $ \x => injective $ prf $ FS x)
-pointwise {f = Drop f} {g = Id} prf = void $ absurd $ prf FZ
-pointwise {f = Drop f} {g = Drop g} prf = DropDrop (pointwise $ \x => injective $ prf x)
-pointwise {f = Drop f} {g = Keep g} prf = void $ absurd $ prf FZ
-pointwise {f = Keep f} {g = Id} prf = KeepId (pointwise $ \x => injective $ prf $ FS x)
-pointwise {f = Keep f} {g = Drop g} prf = void $ absurd $ prf FZ
-pointwise {f = Keep f} {g = Keep g} prf = KeepKeep (pointwise $ \x => injective $ prf $ FS x)
+(.index) : f ~~~ g -> (i : Var ctx1 v) -> index f i = index g i
+prf.index i = prf.indexPos i.pos
 
 --------------------------------------------------------------------------------
 -- Environments ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 public export
-data Env : Nat -> Nat -> Type -> Type where
-  Base : k `Thins` n -> Env k n a
-  (:<) : Env k n a -> a -> Env (S k) n a
+data Env : Context a -> Context a -> (a -> Type) -> Type where
+  Base : {0 ctx1, ctx2 : Context a} -> ctx1 `Thins` ctx2 -> Env ctx1 ctx2 p
+  (:<) :
+    {0 ctx1, ctx2 : Context a} ->
+    Env ctx1 ctx2 p -> (x : Assoc0 (p v)) ->
+    Env (ctx1 :< (x.name :- v)) ctx2 p
 
 %name Env env
 
+lookupPos : Env ctx1 ctx2 p -> VarPos ctx1 x v -> Either (Var ctx2 v) (p v)
+lookupPos (Base f) pos = Left (indexPos f pos)
+lookupPos (env :< (x :- pv)) Here = Right pv
+lookupPos (env :< (x :- pv)) (There pos) = lookupPos env pos
+
 export
-lookup : Env k n a -> Fin k -> Either (Fin n) a
-lookup (Base f) x = Left (index f x)
-lookup (env :< v) FZ = Right v
-lookup (env :< v) (FS x) = lookup env x
+lookup : Env ctx1 ctx2 p -> Var ctx1 v -> Either (Var ctx2 v) (p v)
+lookup env i = lookupPos env i.pos
 
 -- Properties
 
 export
-lookupFZ : (0 env : Env k n a) -> (0 v : a) -> lookup (env :< v) FZ = Right v
-lookupFZ env v = Refl
+lookupHere :
+  (0 env : Env ctx1 ctx2 p) -> (0 x : String) -> (0 pv : p v) ->
+  lookup (env :< (x :- pv)) (%% x) = Right pv
+lookupHere env x pv = Refl
 
 export
 lookupFS :
-  (0 env : Env k n a) -> (0 v : a) -> (0 x : Fin k) ->
-  lookup (env :< v) (FS x) = lookup env x
-lookupFS env v x = Refl
+  (0 env : Env ctx1 ctx2 p) -> (0 x : String) -> (0 pv : p v) -> (0 i : Var ctx1 w) ->
+  lookup (env :< (x :- pv)) (ThereVar i) = lookup env i
+lookupFS env x pv i = Refl
 
 --------------------------------------------------------------------------------
 -- Renaming Coalgebras ---------------------------------------------------------
 --------------------------------------------------------------------------------
 
 public export
-interface Rename (0 a : Nat -> Type) where
-  var : Fin n -> a n
-  rename : k `Thins` n -> a k -> a n
-  0 renameCong : {0 f, g : k `Thins` n} -> f ~~~ g -> (x : a k) -> rename f x = rename g x
-  0 renameId : (x : a n) -> rename Id x = x
-
-export
-lift : Rename a => k `Thins` n -> Env j k (a k) -> Env j n (a n)
+interface Rename (0 a : Type) (0 t : Context a -> a -> Type) where
+  var : {0 ctx : Context a} -> {0 v : a} -> Var ctx v -> t ctx v
+  rename :
+    {0 ctx1, ctx2 : Context a} -> ctx1 `Thins` ctx2 ->
+    {0 v : a} -> t ctx1 v -> t ctx2 v
+  0 renameCong :
+    {0 ctx1, ctx2 : Context a} -> {0 f, g : ctx1 `Thins` ctx2} -> f ~~~ g ->
+    {0 v : a} -> (x : t ctx1 v) -> rename f x = rename g x
+  0 renameId : {0 ctx : Context a} -> {0 v : a} -> (x : t ctx v) -> rename Id x = x
+
+export
+lift : Rename a t => ctx2 `Thins` ctx3 -> Env ctx1 ctx2 (t ctx2) -> Env ctx1 ctx3 (t ctx3)
 lift Id env = env
 lift f (Base g) = Base (f . g)
-lift f (env :< v) = lift f env :< rename f v
+lift f (env :< (x :- v)) = lift f env :< (x :- rename f v)
+
+lookupPosLift :
+  Rename a t =>
+  (f : ctx2 `Thins` ctx3) -> (env : Env ctx1 ctx2 (t ctx2)) -> (pos : VarPos ctx1 x v) ->
+  lookupPos (lift f env) pos = bimap (index f) (rename f) (lookupPos env pos)
+lookupPosLift Id env pos with (lookupPos env pos)
+  _ | Left (%% y) = Refl
+  _ | Right y = cong Right $ irrelevantEq $ sym $ renameId y
+lookupPosLift (Drop f) (Base g) pos = cong Left $ indexPosComp (Drop f) g pos
+lookupPosLift (Keep f) (Base g) pos = cong Left $ indexPosComp (Keep f) g pos
+lookupPosLift (Drop f) (env :< (x :- v)) Here = Refl
+lookupPosLift (Keep f) (env :< (x :- v)) Here = Refl
+lookupPosLift (Drop f) (env :< (x :- v)) (There pos) = lookupPosLift (Drop f) env pos
+lookupPosLift (Keep f) (env :< (x :- v)) (There pos) = lookupPosLift (Keep f) env pos
 
 export
 lookupLift :
-  Rename a =>
-  (f : k `Thins` n) -> (env : Env j k (a k)) -> (x : Fin j) ->
-  lookup (lift f env) x = bimap (index f) (rename f) (lookup env x)
-lookupLift Id env x with (lookup env x)
-  _ | Left y = Refl
-  _ | Right y = cong Right $ irrelevantEq $ sym $ renameId y
-lookupLift (Drop f) (Base g) x = cong Left $ indexComp (Drop f) g x
-lookupLift (Drop f) (env :< y) FZ = Refl
-lookupLift (Drop f) (env :< y) (FS x) = lookupLift (Drop f) env x
-lookupLift (Keep f) (Base g) x = cong Left $ indexComp (Keep f) g x
-lookupLift (Keep f) (env :< y) FZ = Refl
-lookupLift (Keep f) (env :< y) (FS x) = lookupLift (Keep f) env x
+  Rename a t =>
+  (f : ctx2 `Thins` ctx3) -> (env : Env ctx1 ctx2 (t ctx2)) -> (i : Var ctx1 v) ->
+  lookup (lift f env) i = bimap (index f) (rename f) (lookup env i)
+lookupLift f env i = lookupPosLift f env i.pos
diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index 3021f96..e3eee12 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -1,1022 +1,408 @@
 module Inky.Type
 
-import public Data.List1
-
-import Control.Function
 import Data.Bool.Decidable
-import Data.Either
+import Data.DPair
+import Data.Maybe.Decidable
 import Data.These
 import Data.These.Decidable
-import Decidable.Equality
+import Inky.Context
 import Inky.Thinning
 
--- Utilities -------------------------------------------------------------------
-
-reflectFinEq : (i, j : Fin n) -> (i = j) `Reflects` (i == j)
-reflectFinEq FZ FZ = RTrue Refl
-reflectFinEq FZ (FS j) = RFalse absurd
-reflectFinEq (FS i) FZ = RFalse absurd
-reflectFinEq (FS i) (FS j) =
-  viaEquivalence (MkEquivalence (\prf => cong FS prf) injective)
-    (reflectFinEq i j)
-
 -- Definition ------------------------------------------------------------------
 
 public export
-data Ty : Nat -> Type where
-  TVar : Fin n -> Ty n
-  TNat : Ty n
-  TArrow : Ty n -> Ty n -> Ty n
-  TUnion : List1 (Ty n) -> Ty n
-  TProd : List (Ty n) -> Ty n
-  TSum : List (Ty n) -> Ty n
-  TFix : Ty (S n) -> Ty n
+data Ty : Context () -> () -> Type where
+  TVar : Var ctx v -> Ty ctx v
+  TNat : Ty ctx ()
+  TArrow : Ty ctx () -> Ty ctx () -> Ty ctx ()
+  TProd : Row (Ty ctx ()) -> Ty ctx ()
+  TSum : Row (Ty ctx ()) -> Ty ctx ()
+  TFix : (x : String) -> Ty (ctx :< (x :- ())) () -> Ty ctx ()
 
 %name Ty a, b, c
 
-export
-Injective TVar where
-  injective Refl = Refl
+--------------------------------------------------------------------------------
+-- Thinning --------------------------------------------------------------------
+--------------------------------------------------------------------------------
 
-export
-Injective TUnion where
-  injective Refl = Refl
+thin : ctx1 `Thins` ctx2 -> forall v. Ty ctx1 v -> Ty ctx2 v
+thinAll : ctx1 `Thins` ctx2 -> forall v. Row (Ty ctx1 v) -> Row (Ty ctx2 v)
+thinAllFresh :
+  (f : ctx1 `Thins` ctx2) -> (x : String) ->
+  forall v. (row : Row (Ty ctx1 v)) ->
+  So (x `freshIn` row) -> So (x `freshIn` thinAll f row)
 
-export
-Injective TProd where
-  injective Refl = Refl
+thin f (TVar i) = TVar (index f i)
+thin f TNat = TNat
+thin f (TArrow a b) = TArrow (thin f a) (thin f b)
+thin f (TProd as) = TProd (thinAll f as)
+thin f (TSum as) = TSum (thinAll f as)
+thin f (TFix x a) = TFix x (thin (Keep f) a)
 
--- Equality --------------------------------------------------------------------
+thinAll f [<] = [<]
+thinAll f ((:<) as (x :- a) {fresh}) =
+  (:<) (thinAll f as) (x :- thin f a) {fresh = thinAllFresh f x as fresh}
+
+thinAllFresh f x [<] = id
+thinAllFresh f x (as :< (y :- a)) = andSo . mapSnd (thinAllFresh f x as) . soAnd
+
+-- Renaming Coalgebra
+
+thinCong : f ~~~ g -> forall v. (a : Ty ctx1 v) -> thin f a = thin g a
+thinCongAll : f ~~~ g -> forall v. (as : Row (Ty ctx1 v)) -> thinAll f as = thinAll g as
+
+thinCong prf (TVar i) = cong TVar (prf.index i)
+thinCong prf TNat = Refl
+thinCong prf (TArrow a b) = cong2 TArrow (thinCong prf a) (thinCong prf b)
+thinCong prf (TProd as) = cong TProd (thinCongAll prf as)
+thinCong prf (TSum as) = cong TSum (thinCongAll prf as)
+thinCong prf (TFix x a) = cong (TFix x) (thinCong (KeepKeep prf) a)
+
+thinCongAll prf [<] = Refl
+thinCongAll prf (as :< (x :- a)) =
+  snocCong2 (thinCongAll prf as) (cong (x :-) $ thinCong prf a)
+
+thinId : (a : Ty ctx v) -> thin Id a = a
+thinIdAll : (as : Row (Ty ctx v)) -> thinAll Id as = as
+
+thinId (TVar i) = cong TVar (indexId i)
+thinId TNat = Refl
+thinId (TArrow a b) = cong2 TArrow (thinId a) (thinId b)
+thinId (TProd as) = cong TProd (thinIdAll as)
+thinId (TSum as) = cong TSum (thinIdAll as)
+thinId (TFix x a) = cong (TFix x) (trans (thinCong (KeepId IdId) a) (thinId a))
+
+thinIdAll [<] = Refl
+thinIdAll (as :< (x :- a)) =
+  snocCong2 (thinIdAll as) (cong (x :-) $ thinId a)
 
 export
-eq : Ty n -> Ty n -> Bool
-eqAll : List (Ty n) -> List (Ty n) -> Bool
-eqAll1 : List1 (Ty n) -> List1 (Ty n) -> Bool
+Rename () Ty where
+  var = TVar
+  rename = thin
+  renameCong = thinCong
+  renameId = thinId
 
-TVar i `eq` TVar j = i == j
-TNat `eq` TNat = True
-TArrow a b `eq` TArrow c d = (a `eq` c) && (b `eq` d)
-TUnion as `eq` TUnion bs = as `eqAll1` bs
-TProd as `eq` TProd bs = as `eqAll` bs
-TSum as `eq` TSum bs = as `eqAll` bs
-TFix a `eq` TFix b = a `eq` b
-_ `eq` _ = False
+-- Equality --------------------------------------------------------------------
 
-[] `eqAll` [] = True
-(a :: as) `eqAll` (b :: bs) = (a `eq` b) && (as `eqAll` bs)
-_ `eqAll` _ = False
+Preeq :
+  {ctx2 : Context ()} -> {v : ()} ->
+  Ty ctx1 v -> Ty ctx2 v -> ctx1 `Thins` ctx2 -> Type
+PreeqAll :
+  {ctx2 : Context ()} -> {v : ()} ->
+  Row (Ty ctx1 v) -> Row (Ty ctx2 v) -> ctx1 `Thins` ctx2 -> Type
+
+Preeq (TVar i) (TVar j) f = index f i = j
+Preeq (TNat) (TNat) f = ()
+Preeq (TArrow a b) (TArrow c d) f = (Preeq a c f, Preeq b d f)
+Preeq (TProd as) (TProd bs) f = PreeqAll as bs f
+Preeq (TSum as) (TSum bs) f = PreeqAll as bs f
+Preeq (TFix x a) (TFix y b) f = Preeq a b (Keep f)
+Preeq _ _ f = Void
+
+PreeqAll [<] bs f = (bs = [<])
+PreeqAll (as :< (x :- a)) bs f =
+  ( b ** cs **
+  ( Remove x bs b cs
+  , Preeq a b f
+  , PreeqAll as cs f
+  ))
+
+preeqAllReorder :
+  (as : Row (Ty ctx1 v)) -> bs <~> cs -> (f : ctx1 `Thins` ctx2) ->
+  PreeqAll as bs f -> PreeqAll as cs f
+preeqAllReorder [<] [] f Refl = Refl
+preeqAllReorder [<] (step :: prf) f Refl impossible
+preeqAllReorder (as :< (x :- a)) prf f (b ** bs ** (prf', eq1, eq2)) =
+  (b ** bs ** (bimap id (trans (sym prf)) prf', eq1, eq2))
+
+preeq : Ty ctx1 v -> Ty ctx2 v -> ctx1 `Thins` ctx2 -> Bool
+preeqAll : Row (Ty ctx1 v) -> Row (Ty ctx2 v) -> ctx1 `Thins` ctx2 -> Bool
+
+preeq (TVar i) (TVar j) f = index f i == j
+preeq TNat TNat f = True
+preeq (TArrow a b) (TArrow c d) f = preeq a c f && preeq b d f
+preeq (TProd as) (TProd bs) f = preeqAll as bs f
+preeq (TSum as) (TSum bs) f = preeqAll as bs f
+preeq (TFix x a) (TFix y b) f = preeq a b (Keep f)
+preeq _ _ f = False
+
+preeqAll [<] bs f = null bs
+preeqAll (as :< (x :- a)) bs f =
+  case remove' x bs of
+    Just (b, bs) => preeq a b f && preeqAll as bs f
+    Nothing => False
 
-(a ::: as) `eqAll1` (b ::: bs) = (a `eq` b) && (as `eqAll` bs)
+export
+reflectAnd : a `Reflects` b1 -> b `Reflects` b2 -> (a, b) `Reflects` (b1 && b2)
+reflectAnd (RTrue x) (RTrue y) = RTrue (x, y)
+reflectAnd (RTrue x) (RFalse f) = RFalse (f . snd)
+reflectAnd (RFalse f) _ = RFalse (f . fst)
+
+0 reflectPreeq :
+  (a : Ty ctx1 v) -> (b : Ty ctx2 v) -> (f : ctx1 `Thins` ctx2) ->
+  Preeq a b f `Reflects` preeq a b f
+0 reflectPreeqAll :
+  (as : Row (Ty ctx1 v)) -> (bs : Row (Ty ctx2 v)) -> (f : ctx1 `Thins` ctx2) ->
+  PreeqAll as bs f `Reflects` preeqAll as bs f
+
+reflectPreeq (TVar i) (TVar j) f = reflectEq (index f i) j
+reflectPreeq (TVar i) TNat f = RFalse id
+reflectPreeq (TVar i) (TArrow a b) f = RFalse id
+reflectPreeq (TVar i) (TProd as) f = RFalse id
+reflectPreeq (TVar i) (TSum as) f = RFalse id
+reflectPreeq (TVar i) (TFix x a) f = RFalse id
+reflectPreeq TNat (TVar i) f = RFalse id
+reflectPreeq TNat TNat f = RTrue ()
+reflectPreeq TNat (TArrow a b) f = RFalse id
+reflectPreeq TNat (TProd as) f = RFalse id
+reflectPreeq TNat (TSum as) f = RFalse id
+reflectPreeq TNat (TFix x a) f = RFalse id
+reflectPreeq (TArrow a c) (TVar i) f = RFalse id
+reflectPreeq (TArrow a c) TNat f = RFalse id
+reflectPreeq (TArrow a c) (TArrow b d) f = reflectAnd (reflectPreeq a b f) (reflectPreeq c d f)
+reflectPreeq (TArrow a c) (TProd as) f = RFalse id
+reflectPreeq (TArrow a c) (TSum as) f = RFalse id
+reflectPreeq (TArrow a c) (TFix x b) f = RFalse id
+reflectPreeq (TProd as) (TVar i) f = RFalse id
+reflectPreeq (TProd as) TNat f = RFalse id
+reflectPreeq (TProd as) (TArrow a b) f = RFalse id
+reflectPreeq (TProd as) (TProd bs) f = reflectPreeqAll as bs f
+reflectPreeq (TProd as) (TSum bs) f = RFalse id
+reflectPreeq (TProd as) (TFix x a) f = RFalse id
+reflectPreeq (TSum as) (TVar i) f = RFalse id
+reflectPreeq (TSum as) TNat f = RFalse id
+reflectPreeq (TSum as) (TArrow a b) f = RFalse id
+reflectPreeq (TSum as) (TProd bs) f = RFalse id
+reflectPreeq (TSum as) (TSum bs) f = reflectPreeqAll as bs f
+reflectPreeq (TSum as) (TFix x a) f = RFalse id
+reflectPreeq (TFix x a) (TVar i) f = RFalse id
+reflectPreeq (TFix x a) TNat f = RFalse id
+reflectPreeq (TFix x a) (TArrow b c) f = RFalse id
+reflectPreeq (TFix x a) (TProd as) f = RFalse id
+reflectPreeq (TFix x a) (TSum as) f = RFalse id
+reflectPreeq (TFix x a) (TFix y b) f = reflectPreeq a b (Keep f)
+
+reflectPreeqAll [<] [<] f = RTrue Refl
+reflectPreeqAll [<] (_ :< _) f = RFalse (\case Refl impossible)
+reflectPreeqAll (as :< (x :- a)) bs f with (reflectRemove x bs) | (remove' x bs)
+  _ | RJust (Evidence fresh prf) | Just (b, cs) with (reflectAnd (reflectPreeq a b f) (reflectPreeqAll as cs f)) | (preeq a b f && preeqAll as cs f)
+    _ | RTrue prf' | _ = RTrue (b ** cs ** (Evidence fresh prf, prf'))
+    _ | RFalse nprf | _ =
+      RFalse (\(b' ** cs' ** (prf1, prf2)) =>
+        let (eq, reorder) = removeUnique x bs (Evidence fresh prf) prf1 in
+        nprf $
+        bimap
+          (\x => rewrite eq in x)
+          (preeqAllReorder as (sym reorder) f)
+          prf2)
+  _ | RNothing nprf | _ = RFalse (\(b ** cs ** (prf, _)) => nprf (b, cs) prf)
 
 public export
-Eq (Ty n) where
-  (==) = eq
+Eq (Ty ctx v) where
+  a == b = preeq a b Id
 
 export
-reflectEq : (a, b : Ty n) -> (a = b) `Reflects` (a `eq` b)
-reflectEqAll : (as, bs : List (Ty n)) -> (as = bs) `Reflects` (as `eqAll` bs)
-reflectEqAll1 : (as, bs : List1 (Ty n)) -> (as = bs) `Reflects` (as `eqAll1` bs)
-
-reflectEq (TVar i) (TVar j) with (reflectFinEq i j) | (i == j)
-  _ | RTrue eq | _ = RTrue (cong TVar eq)
-  _ | RFalse neq | _ = RFalse (\eq => neq $ injective eq)
-reflectEq (TVar i) TNat = RFalse (\case Refl impossible)
-reflectEq (TVar i) (TArrow c d) = RFalse (\case Refl impossible)
-reflectEq (TVar i) (TUnion c) = RFalse (\case Refl impossible)
-reflectEq (TVar i) (TProd c) = RFalse (\case Refl impossible)
-reflectEq (TVar i) (TSum c) = RFalse (\case Refl impossible)
-reflectEq (TVar i) (TFix b) = RFalse (\case Refl impossible)
-reflectEq TNat (TVar j) = RFalse (\case Refl impossible)
-reflectEq TNat TNat = RTrue Refl
-reflectEq TNat (TArrow c d) = RFalse (\case Refl impossible)
-reflectEq TNat (TUnion c) = RFalse (\case Refl impossible)
-reflectEq TNat (TProd c) = RFalse (\case Refl impossible)
-reflectEq TNat (TSum c) = RFalse (\case Refl impossible)
-reflectEq TNat (TFix b) = RFalse (\case Refl impossible)
-reflectEq (TArrow a b) (TVar j) = RFalse (\case Refl impossible)
-reflectEq (TArrow a b) TNat = RFalse (\case Refl impossible)
-reflectEq (TArrow a b) (TArrow c d) with (reflectEq a c) | (a `eq` c)
-  _ | RTrue eq1 | _ with (reflectEq b d) | (b `eq` d)
-    _ | RTrue eq2 | _ = RTrue (cong2 TArrow eq1 eq2)
-    _ | RFalse neq2 | _ = RFalse (\case Refl => neq2 Refl)
-  _ | RFalse neq1 | _ = RFalse (\case Refl => neq1 Refl)
-reflectEq (TArrow a b) (TUnion c) = RFalse (\case Refl impossible)
-reflectEq (TArrow a b) (TProd c) = RFalse (\case Refl impossible)
-reflectEq (TArrow a b) (TSum c) = RFalse (\case Refl impossible)
-reflectEq (TArrow a b) (TFix c) = RFalse (\case Refl impossible)
-reflectEq (TUnion as) (TVar j) = RFalse (\case Refl impossible)
-reflectEq (TUnion as) TNat = RFalse (\case Refl impossible)
-reflectEq (TUnion as) (TArrow c d) = RFalse (\case Refl impossible)
-reflectEq (TUnion as) (TUnion c) with (reflectEqAll1 as c) | (as `eqAll1` c)
-  _ | RTrue eq | _ = RTrue (cong TUnion eq)
-  _ | RFalse neq | _ = RFalse (\case Refl => neq Refl)
-reflectEq (TUnion as) (TProd c) = RFalse (\case Refl impossible)
-reflectEq (TUnion as) (TSum c) = RFalse (\case Refl impossible)
-reflectEq (TUnion as) (TFix b) = RFalse (\case Refl impossible)
-reflectEq (TProd as) (TVar j) = RFalse (\case Refl impossible)
-reflectEq (TProd as) TNat = RFalse (\case Refl impossible)
-reflectEq (TProd as) (TArrow c d) = RFalse (\case Refl impossible)
-reflectEq (TProd as) (TUnion c) = RFalse (\case Refl impossible)
-reflectEq (TProd as) (TProd c) with (reflectEqAll as c) | (as `eqAll` c)
-  _ | RTrue eq | _ = RTrue (cong TProd eq)
-  _ | RFalse neq | _ = RFalse (\case Refl => neq Refl)
-reflectEq (TProd as) (TSum c) = RFalse (\case Refl impossible)
-reflectEq (TProd as) (TFix b) = RFalse (\case Refl impossible)
-reflectEq (TSum as) (TVar j) = RFalse (\case Refl impossible)
-reflectEq (TSum as) TNat = RFalse (\case Refl impossible)
-reflectEq (TSum as) (TArrow c d) = RFalse (\case Refl impossible)
-reflectEq (TSum as) (TUnion c) = RFalse (\case Refl impossible)
-reflectEq (TSum as) (TProd c) = RFalse (\case Refl impossible)
-reflectEq (TSum as) (TSum c) with (reflectEqAll as c) | (as `eqAll` c)
-  _ | RTrue eq | _ = RTrue (cong TSum eq)
-  _ | RFalse neq | _ = RFalse (\case Refl => neq Refl)
-reflectEq (TSum as) (TFix b) = RFalse (\case Refl impossible)
-reflectEq (TFix a) (TVar j) = RFalse (\case Refl impossible)
-reflectEq (TFix a) TNat = RFalse (\case Refl impossible)
-reflectEq (TFix a) (TArrow c d) = RFalse (\case Refl impossible)
-reflectEq (TFix a) (TUnion c) = RFalse (\case Refl impossible)
-reflectEq (TFix a) (TProd c) = RFalse (\case Refl impossible)
-reflectEq (TFix a) (TSum c) = RFalse (\case Refl impossible)
-reflectEq (TFix a) (TFix b) with (reflectEq a b) | (a `eq` b)
-  _ | RTrue eq | _ = RTrue (cong TFix eq)
-  _ | RFalse neq | _ = RFalse (\case Refl => neq Refl)
-
-reflectEqAll [] [] = RTrue Refl
-reflectEqAll [] (b :: bs) = RFalse (\case Refl impossible)
-reflectEqAll (a :: as) [] = RFalse (\case Refl impossible)
-reflectEqAll (a :: as) (b :: bs) with (reflectEq a b) | (a `eq` b)
-  _ | RTrue eq1 | _ with (reflectEqAll as bs) | (as `eqAll` bs)
-    _ | RTrue eq2 | _ = RTrue (cong2 (::) eq1 eq2)
-    _ | RFalse neq2 | _ = RFalse (\case Refl => neq2 Refl)
-  _ | RFalse neq1 | _ = RFalse (\case Refl => neq1 Refl)
-
-reflectEqAll1 (a ::: as) (b ::: bs) with (reflectEq a b) | (a `eq` b)
-  _ | RTrue eq1 | _ with (reflectEqAll as bs) | (as `eqAll` bs)
-    _ | RTrue eq2 | _ = RTrue (cong2 (:::) eq1 eq2)
-    _ | RFalse neq2 | _ = RFalse (\case Refl => neq2 Refl)
-  _ | RFalse neq1 | _ = RFalse (\case Refl => neq1 Refl)
+Eq : {ctx : Context ()} -> {v : ()} -> Ty ctx v -> Ty ctx v -> Type
+Eq a b = Preeq a b Id
+
+export
+0 reflectEq : (a, b : Ty ctx v) -> (a `Eq` b) `Reflects` (a == b)
+reflectEq a b = reflectPreeq a b Id
 
 -- Occurs ----------------------------------------------------------------------
 
-OccursIn : Fin n -> Ty n -> Type
-OccursInAny : Fin n -> List (Ty n) -> Type
-OccursInAny1 : Fin n -> List1 (Ty n) -> Type
+OccursIn : Var ctx v -> Ty ctx w -> Type
+OccursInAny : Var ctx v -> Row (Ty ctx w) -> Type
 
 i `OccursIn` TVar j = i = j
 i `OccursIn` TNat = Void
 i `OccursIn` TArrow a b = These (i `OccursIn` a) (i `OccursIn` b)
-i `OccursIn` TUnion as = i `OccursInAny1` as
 i `OccursIn` TProd as = i `OccursInAny` as
 i `OccursIn` TSum as = i `OccursInAny` as
-i `OccursIn` TFix a = FS i `OccursIn` a
+i `OccursIn` TFix x a = ThereVar i `OccursIn` a
 
-i `OccursInAny` [] = Void
-i `OccursInAny` a :: as = These (i `OccursIn` a) (i `OccursInAny` as)
-
-i `OccursInAny1` a ::: as = These (i `OccursIn` a) (i `OccursInAny` as)
+i `OccursInAny` [<] = Void
+i `OccursInAny` (as :< (x :- a)) = These (i `OccursIn` a) (i `OccursInAny` as)
 
 -- Decidable
 
-occursIn : (i : Fin n) -> (a : Ty n) -> Bool
-occursInAny : (i : Fin n) -> (as : List (Ty n)) -> Bool
-occursInAny1 : (i : Fin n) -> (as : List1 (Ty n)) -> Bool
+occursIn : (i : Var ctx v) -> (a : Ty ctx w) -> Bool
+occursInAny : (i : Var ctx v) -> (as : Row (Ty ctx w)) -> Bool
 
-reflectOccursIn :
-  (i : Fin n) -> (a : Ty n) ->
-  (i `OccursIn` a) `Reflects` (i `occursIn` a)
-reflectOccursInAny :
-  (i : Fin n) -> (as : List (Ty n)) ->
-  (i `OccursInAny` as) `Reflects` (i `occursInAny` as)
-reflectOccursInAny1 :
-  (i : Fin n) -> (as : List1 (Ty n)) ->
-  (i `OccursInAny1` as) `Reflects` (i `occursInAny1` as)
-
-i `occursIn` (TVar j) = i == j
+i `occursIn` (TVar j) = i `eq` j
 i `occursIn` TNat = False
 i `occursIn` (TArrow a b) = (i `occursIn` a) || (i `occursIn` b)
-i `occursIn` (TUnion as) = i `occursInAny1` as
 i `occursIn` (TProd as) = i `occursInAny` as
 i `occursIn` (TSum as) = i `occursInAny` as
-i `occursIn` (TFix a) = FS i `occursIn` a
+i `occursIn` (TFix x a) = ThereVar i `occursIn` a
 
-i `occursInAny` [] = False
-i `occursInAny` (a :: as) = (i `occursIn` a) || (i `occursInAny` as)
+i `occursInAny` [<] = False
+i `occursInAny` (as :< (x :- a)) = (i `occursIn` a) || (i `occursInAny` as)
 
-i `occursInAny1` (a ::: as) = (i `occursIn` a) || (i `occursInAny` as)
+reflectOccursIn :
+  (i : Var ctx v) -> (a : Ty ctx w) ->
+  (i `OccursIn` a) `Reflects` (i `occursIn` a)
+reflectOccursInAny :
+  (i : Var ctx v) -> (as : Row (Ty ctx w)) ->
+  (i `OccursInAny` as) `Reflects` (i `occursInAny` as)
 
-reflectOccursIn i (TVar j) = reflectFinEq i j
+reflectOccursIn i (TVar j) = reflectEq i j
 reflectOccursIn i TNat = RFalse id
 reflectOccursIn i (TArrow a b) = reflectThese (reflectOccursIn i a) (reflectOccursIn i b)
-reflectOccursIn i (TUnion as) = reflectOccursInAny1 i as
 reflectOccursIn i (TProd as) = reflectOccursInAny i as
 reflectOccursIn i (TSum as) = reflectOccursInAny i as
-reflectOccursIn i (TFix a) = reflectOccursIn (FS i) a
-
-reflectOccursInAny i [] = RFalse id
-reflectOccursInAny i (a :: as) = reflectThese (reflectOccursIn i a) (reflectOccursInAny i as)
+reflectOccursIn i (TFix x a) = reflectOccursIn (ThereVar i) a
 
-reflectOccursInAny1 i (a ::: as) = reflectThese (reflectOccursIn i a) (reflectOccursInAny i as)
+reflectOccursInAny i [<] = RFalse id
+reflectOccursInAny i (as :< (x :- a)) =
+  reflectThese (reflectOccursIn i a) (reflectOccursInAny i as)
 
 -- Not Strictly Positive -----------------------------------------------------------
 
 -- We use negation so we get a cause on failure.
 
-NotPositiveIn : Fin n -> Ty n -> Type
-NotPositiveInAny : Fin n -> List (Ty n) -> Type
-NotPositiveInAny1 : Fin n -> List1 (Ty n) -> Type
+NotPositiveIn : Var ctx v -> Ty ctx w -> Type
+NotPositiveInAny : Var ctx v -> Row (Ty ctx w) -> Type
 
 i `NotPositiveIn` TVar j = Void
 i `NotPositiveIn` TNat = Void
-i `NotPositiveIn` TArrow a b = These (i `OccursIn` a) (i `NotPositiveIn` b)
-i `NotPositiveIn` TUnion as = i `NotPositiveInAny1` as
+i `NotPositiveIn` TArrow a b =
+  -- NOTE: forbid on right side of arrow to prevent infinite breadth.
+  i `OccursIn` TArrow a b
 i `NotPositiveIn` TProd as = i `NotPositiveInAny` as
 i `NotPositiveIn` TSum as = i `NotPositiveInAny` as
-i `NotPositiveIn` TFix a = FS i `OccursIn` a
-  -- Prevent mutual recursion;
-  -- Can add back in without breaking things
+i `NotPositiveIn` TFix x a =
+  -- BUG: forbid under fixpoint to prevent unbounded width
+  -- this is safe to add back with the complex encoding of fixpoints
+  ThereVar i `OccursIn` a
 
-i `NotPositiveInAny` [] = Void
-i `NotPositiveInAny` a :: as = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as)
-
-i `NotPositiveInAny1` a ::: as = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as)
+i `NotPositiveInAny` [<] = Void
+i `NotPositiveInAny` as :< (x :- a) = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as)
 
 -- Not Positive implies Occurs
 
-notPositiveToOccurs : (a : Ty k) -> i `NotPositiveIn` a -> i `OccursIn` a
-notPositiveAnyToOccursAny : (as : List (Ty k)) -> i `NotPositiveInAny` as -> i `OccursInAny` as
-notPositiveAny1ToOccursAny1 : (as : List1 (Ty k)) -> i `NotPositiveInAny1` as -> i `OccursInAny1` as
+notPositiveToOccurs : (a : Ty ctx v) -> i `NotPositiveIn` a -> i `OccursIn` a
+notPositiveAnyToOccursAny : (as : Row (Ty ctx v)) -> i `NotPositiveInAny` as -> i `OccursInAny` as
 
 notPositiveToOccurs (TVar j) = absurd
 notPositiveToOccurs TNat = id
-notPositiveToOccurs (TArrow a b) = mapSnd (notPositiveToOccurs b)
-notPositiveToOccurs (TUnion as) = notPositiveAny1ToOccursAny1 as
+notPositiveToOccurs (TArrow a b) = id
 notPositiveToOccurs (TProd as) = notPositiveAnyToOccursAny as
 notPositiveToOccurs (TSum as) = notPositiveAnyToOccursAny as
-notPositiveToOccurs (TFix a) = id
-
-notPositiveAnyToOccursAny [] = id
-notPositiveAnyToOccursAny (a :: as) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as)
+notPositiveToOccurs (TFix x a) = id
 
-notPositiveAny1ToOccursAny1 (a ::: as) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as)
-
--- Decidable
+notPositiveAnyToOccursAny [<] = id
+notPositiveAnyToOccursAny (as :< (x :- a)) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as)
 
-notEnvPositiveIn : (i : Fin n) -> (a : Ty n) -> Bool
-notEnvPositiveInAny : (i : Fin n) -> (as : List (Ty n)) -> Bool
-notEnvPositiveInAny1 : (i : Fin n) -> (as : List1 (Ty n)) -> Bool
+-- -- Decidable
 
-i `notEnvPositiveIn` (TVar j) = False
-i `notEnvPositiveIn` TNat = False
-i `notEnvPositiveIn` (TArrow a b) = (i `occursIn` a) || (i `notEnvPositiveIn` b)
-i `notEnvPositiveIn` (TUnion as) = i `notEnvPositiveInAny1` as
-i `notEnvPositiveIn` (TProd as) = i `notEnvPositiveInAny` as
-i `notEnvPositiveIn` (TSum as) = i `notEnvPositiveInAny` as
-i `notEnvPositiveIn` (TFix a) = FS i `occursIn` a
+notPositiveIn : (i : Var ctx v) -> (a : Ty ctx w) -> Bool
+notPositiveInAny : (i : Var ctx v) -> (as : Row (Ty ctx w)) -> Bool
 
-i `notEnvPositiveInAny` [] = False
-i `notEnvPositiveInAny` (a :: as) = (i `notEnvPositiveIn` a) || (i `notEnvPositiveInAny` as)
+i `notPositiveIn` (TVar j) = False
+i `notPositiveIn` TNat = False
+i `notPositiveIn` (TArrow a b) = i `occursIn` TArrow a b
+i `notPositiveIn` (TProd as) = i `notPositiveInAny` as
+i `notPositiveIn` (TSum as) = i `notPositiveInAny` as
+i `notPositiveIn` (TFix x a) = ThereVar i `occursIn` a
 
-i `notEnvPositiveInAny1` (a ::: as) = (i `notEnvPositiveIn` a) || (i `notEnvPositiveInAny` as)
+i `notPositiveInAny` [<] = False
+i `notPositiveInAny` (as :< (x :- a)) = (i `notPositiveIn` a) || (i `notPositiveInAny` as)
 
 reflectNotPositiveIn :
-  (i : Fin n) -> (a : Ty n) ->
-  (i `NotPositiveIn` a) `Reflects` (i `notEnvPositiveIn` a)
+  (i : Var ctx v) -> (a : Ty ctx w) ->
+  (i `NotPositiveIn` a) `Reflects` (i `notPositiveIn` a)
 reflectNotPositiveInAny :
-  (i : Fin n) -> (as : List (Ty n)) ->
-  (i `NotPositiveInAny` as) `Reflects` (i `notEnvPositiveInAny` as)
-reflectNotPositiveInAny1 :
-  (i : Fin n) -> (as : List1 (Ty n)) ->
-  (i `NotPositiveInAny1` as) `Reflects` (i `notEnvPositiveInAny1` as)
+  (i : Var ctx v) -> (as : Row (Ty ctx w)) ->
+  (i `NotPositiveInAny` as) `Reflects` (i `notPositiveInAny` as)
 
 reflectNotPositiveIn i (TVar j) = RFalse id
 reflectNotPositiveIn i TNat = RFalse id
-reflectNotPositiveIn i (TArrow a b) =
-  reflectThese (reflectOccursIn i a) (reflectNotPositiveIn i b)
-reflectNotPositiveIn i (TUnion as) = reflectNotPositiveInAny1 i as
+reflectNotPositiveIn i (TArrow a b) = reflectOccursIn i (TArrow a b)
 reflectNotPositiveIn i (TProd as) = reflectNotPositiveInAny i as
 reflectNotPositiveIn i (TSum as) = reflectNotPositiveInAny i as
-reflectNotPositiveIn i (TFix a) = reflectOccursIn (FS i) a
+reflectNotPositiveIn i (TFix x a) = reflectOccursIn (ThereVar i) a
 
-reflectNotPositiveInAny i [] = RFalse id
-reflectNotPositiveInAny i (a :: as) =
-  reflectThese (reflectNotPositiveIn i a) (reflectNotPositiveInAny i as)
-
-reflectNotPositiveInAny1 i (a ::: as) =
+reflectNotPositiveInAny i [<] = RFalse id
+reflectNotPositiveInAny i (as :< (x :- a)) =
   reflectThese (reflectNotPositiveIn i a) (reflectNotPositiveInAny i as)
 
 -- Well Formed -----------------------------------------------------------------
 
--- Negating reflectidable properties is fun.
+-- Negating decidable properties is fun.
 
 export
-IllFormed : Ty n -> Type
-AnyIllFormed : List (Ty n) -> Type
-Any1IllFormed : List1 (Ty n) -> Type
+IllFormed : Ty ctx v -> Type
+AnyIllFormed : Row (Ty ctx v) -> Type
 
 IllFormed (TVar v) = Void
 IllFormed TNat = Void
 IllFormed (TArrow a b) = These (IllFormed a) (IllFormed b)
-IllFormed (TUnion as) = Any1IllFormed as
 IllFormed (TProd as) = AnyIllFormed as
 IllFormed (TSum as) = AnyIllFormed as
-IllFormed (TFix a) = These (FZ `NotPositiveIn` a) (IllFormed a)
-
-AnyIllFormed [] = Void
-AnyIllFormed (a :: as) = These (IllFormed a) (AnyIllFormed as)
+IllFormed (TFix x a) = These (%% x `NotPositiveIn` a) (IllFormed a)
 
-Any1IllFormed (a ::: as) = These (IllFormed a) (AnyIllFormed as)
+AnyIllFormed [<] = Void
+AnyIllFormed (as :< (x :- a)) = These (IllFormed a) (AnyIllFormed as)
 
 -- Decidable
 
 export
-illFormed : (a : Ty n) -> Bool
-anyIllFormed : (as : List (Ty n)) -> Bool
-any1IllFormed : (as : List1 (Ty n)) -> Bool
-
+illFormed : (a : Ty ctx v) -> Bool
+anyIllFormed : (as : Row (Ty ctx v)) -> Bool
 
 illFormed (TVar j) = False
 illFormed TNat = False
 illFormed (TArrow a b) = illFormed a || illFormed b
-illFormed (TUnion as) = any1IllFormed as
 illFormed (TProd as) = anyIllFormed as
 illFormed (TSum as) = anyIllFormed as
-illFormed (TFix a) = (FZ `notEnvPositiveIn` a) || illFormed a
-
-anyIllFormed [] = False
-anyIllFormed (a :: as) = illFormed a || anyIllFormed as
+illFormed (TFix x a) = (%% x `notPositiveIn` a) || illFormed a
 
-any1IllFormed (a ::: as) = illFormed a || anyIllFormed as
+anyIllFormed [<] = False
+anyIllFormed (as :< (x :- a)) = illFormed a || anyIllFormed as
 
 export
-reflectIllFormed : (a : Ty n) -> IllFormed a `Reflects` illFormed a
-reflectAnyIllFormed : (as : List (Ty n)) -> AnyIllFormed as `Reflects` anyIllFormed as
-reflectAny1IllFormed : (as : List1 (Ty n)) -> Any1IllFormed as `Reflects` any1IllFormed as
+reflectIllFormed : (a : Ty ctx v) -> IllFormed a `Reflects` illFormed a
+reflectAnyIllFormed : (as : Row (Ty ctx v)) -> AnyIllFormed as `Reflects` anyIllFormed as
 
 reflectIllFormed (TVar j) = RFalse id
 reflectIllFormed TNat = RFalse id
-reflectIllFormed (TArrow a b) =
-  reflectThese (reflectIllFormed a) (reflectIllFormed b)
-reflectIllFormed (TUnion as) = reflectAny1IllFormed as
+reflectIllFormed (TArrow a b) = reflectThese (reflectIllFormed a) (reflectIllFormed b)
 reflectIllFormed (TProd as) = reflectAnyIllFormed as
 reflectIllFormed (TSum as) = reflectAnyIllFormed as
-reflectIllFormed (TFix a) = reflectThese (reflectNotPositiveIn FZ a) (reflectIllFormed a)
-
-reflectAnyIllFormed [] = RFalse id
-reflectAnyIllFormed (a :: as) =
-  reflectThese (reflectIllFormed a) (reflectAnyIllFormed as)
+reflectIllFormed (TFix x a) = reflectThese (reflectNotPositiveIn (%% x) a) (reflectIllFormed a)
 
-reflectAny1IllFormed (a ::: as) =
+reflectAnyIllFormed [<] = RFalse id
+reflectAnyIllFormed (as :< (x :- a)) =
   reflectThese (reflectIllFormed a) (reflectAnyIllFormed as)
 
 --------------------------------------------------------------------------------
--- Thinning --------------------------------------------------------------------
---------------------------------------------------------------------------------
-
-thin : k `Thins` n -> Ty k -> Ty n
-thinAll : k `Thins` n -> List (Ty k) -> List (Ty n)
-thinAll1 : k `Thins` n -> List1 (Ty k) -> List1 (Ty n)
-
-thin f (TVar i) = TVar (index f i)
-thin f TNat = TNat
-thin f (TArrow a b) = TArrow (thin f a) (thin f b)
-thin f (TUnion as) = TUnion (thinAll1 f as)
-thin f (TProd as) = TProd (thinAll f as)
-thin f (TSum as) = TSum (thinAll f as)
-thin f (TFix a) = TFix (thin (Keep f) a)
-
-thinAll f [] = []
-thinAll f (a :: as) = thin f a :: thinAll f as
-
-thinAll1 f (a ::: as) = thin f a ::: thinAll f as
-
--- Renaming Coalgebra
-
-thinCong : f ~~~ g -> (a : Ty k) -> thin f a = thin g a
-thinCongAll : f ~~~ g -> (as : List (Ty k)) -> thinAll f as = thinAll g as
-thinCongAll1 : f ~~~ g -> (as : List1 (Ty k)) -> thinAll1 f as = thinAll1 g as
-
-thinCong prf (TVar i) = cong TVar (prf.index i)
-thinCong prf TNat = Refl
-thinCong prf (TArrow a b) = cong2 TArrow (thinCong prf a) (thinCong prf b)
-thinCong prf (TUnion as) = cong TUnion (thinCongAll1 prf as)
-thinCong prf (TProd as) = cong TProd (thinCongAll prf as)
-thinCong prf (TSum as) = cong TSum (thinCongAll prf as)
-thinCong prf (TFix a) = cong TFix (thinCong (KeepKeep prf) a)
-
-thinCongAll prf [] = Refl
-thinCongAll prf (a :: as) = cong2 (::) (thinCong prf a) (thinCongAll prf as)
-
-thinCongAll1 prf (a ::: as) = cong2 (:::) (thinCong prf a) (thinCongAll prf as)
-
-thinId : (a : Ty n) -> thin Id a = a
-thinIdAll : (as : List (Ty n)) -> thinAll Id as = as
-thinIdAll1 : (as : List1 (Ty n)) -> thinAll1 Id as = as
-
-thinId (TVar i) = cong TVar (indexId i)
-thinId TNat = Refl
-thinId (TArrow a b) = cong2 TArrow (thinId a) (thinId b)
-thinId (TUnion as) = cong TUnion (thinIdAll1 as)
-thinId (TProd as) = cong TProd (thinIdAll as)
-thinId (TSum as) = cong TSum (thinIdAll as)
-thinId (TFix a) = cong TFix (trans (thinCong (KeepId IdId) a) (thinId a))
-
-thinIdAll [] = Refl
-thinIdAll (a :: as) = cong2 (::) (thinId a) (thinIdAll as)
-
-thinIdAll1 (a ::: as) = cong2 (:::) (thinId a) (thinIdAll as)
-
-export
-Rename Ty where
-  var = TVar
-  rename = thin
-  renameCong = thinCong
-  renameId = thinId
-
--- Properties ------------------------------------------------------------------
-
--- Occurs --
-
-thinOccursIn :
-  (0 f : k `Thins` n) -> (0 i : Fin k) -> (a : Ty k) ->
-  i `OccursIn` a ->
-  index f i `OccursIn` thin f a
-thinOccursInAny :
-  (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List (Ty k)) ->
-  i `OccursInAny` as ->
-  index f i `OccursInAny` thinAll f as
-thinOccursInAny1 :
-  (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List1 (Ty k)) ->
-  i `OccursInAny1` as ->
-  index f i `OccursInAny1` thinAll1 f as
-
-thinOccursIn f i (TVar x) = \Refl => Refl
-thinOccursIn f i TNat = id
-thinOccursIn f i (TArrow a b) = bimap (thinOccursIn f i a) (thinOccursIn f i b)
-thinOccursIn f i (TUnion as) = thinOccursInAny1 f i as
-thinOccursIn f i (TProd as) = thinOccursInAny f i as
-thinOccursIn f i (TSum as) = thinOccursInAny f i as
-thinOccursIn f i (TFix a) =
-  rewrite sym $ indexKeepFS f i in
-  thinOccursIn (Keep f) (FS i) a
-
-thinOccursInAny f i [] = id
-thinOccursInAny f i (a :: as) = bimap (thinOccursIn f i a) (thinOccursInAny f i as)
-
-thinOccursInAny1 f i (a ::: as) = bimap (thinOccursIn f i a) (thinOccursInAny f i as)
-
--- Inverse
-
-thinOccursInInv' :
-  (0 f : k `Thins` n) -> (0 i : Fin n) ->
-  (a : Ty k) ->
-  i `OccursIn` thin f a ->
-  (j ** (index f j = i, j `OccursIn` a))
-thinOccursInAnyInv' :
-  (0 f : k `Thins` n) -> (0 i : Fin n) ->
-  (as : List (Ty k)) ->
-  i `OccursInAny` thinAll f as ->
-  (j ** (index f j = i, j `OccursInAny` as))
-thinOccursInAny1Inv' :
-  (0 f : k `Thins` n) -> (0 i : Fin n) ->
-  (as : List1 (Ty k)) ->
-  i `OccursInAny1` thinAll1 f as ->
-  (j ** (index f j = i, j `OccursInAny1` as))
-
-thinOccursInInv' f i (TVar j) = \eq => (j ** (sym eq , Refl))
-thinOccursInInv' f i TNat = absurd
-thinOccursInInv' f i (TArrow a b) =
-  these
-    (\occurs =>
-      let (j ** (eq, prf)) = thinOccursInInv' f i a occurs in
-      (j ** (eq, This prf)))
-    (\occurs =>
-      let (j ** (eq, prf)) = thinOccursInInv' f i b occurs in
-      (j ** (eq, That prf)))
-    (\occurs1, occurs2 =>
-      let (j1 ** (eq1, prf1)) = thinOccursInInv' f i a occurs1 in
-      let (j2 ** (eq2, prf2)) = thinOccursInInv' f i b occurs2 in
-      (j1 ** (eq1,
-        Both prf1 $
-        rewrite indexInjective f {x = j1, y = j2} $ trans eq1 (sym eq2) in
-        prf2)))
-thinOccursInInv' f i (TUnion as) = thinOccursInAny1Inv' f i as
-thinOccursInInv' f i (TProd as) = thinOccursInAnyInv' f i as
-thinOccursInInv' f i (TSum as) = thinOccursInAnyInv' f i as
-thinOccursInInv' f i (TFix a) =
-  \occurs =>
-    case thinOccursInInv' (Keep f) (FS i) a occurs of
-      (FZ ** prf) => absurd (trans (sym $ indexKeepFZ f) (fst prf))
-      (FS j ** (eq, prf)) =>
-        (j ** (irrelevantEq (injective $ trans (sym $ indexKeepFS f j) eq), prf))
-
-thinOccursInAnyInv' f i [] = absurd
-thinOccursInAnyInv' f i (a :: as) =
-  these
-    (\occurs =>
-      let (j ** (eq, prf)) = thinOccursInInv' f i a occurs in
-      (j ** (eq, This prf)))
-    (\occurs =>
-      let (j ** (eq, prf)) = thinOccursInAnyInv' f i as occurs in
-      (j ** (eq, That prf)))
-    (\occurs1, occurs2 =>
-      let (j1 ** (eq1, prf1)) = thinOccursInInv' f i a occurs1 in
-      let (j2 ** (eq2, prf2)) = thinOccursInAnyInv' f i as occurs2 in
-      (j1 ** (eq1,
-        Both prf1 $
-        rewrite indexInjective f {x = j1, y = j2} $ trans eq1 (sym eq2) in
-        prf2)))
-
-thinOccursInAny1Inv' f i (a ::: as) =
-  these
-    (\occurs =>
-      let (j ** (eq, prf)) = thinOccursInInv' f i a occurs in
-      (j ** (eq, This prf)))
-    (\occurs =>
-      let (j ** (eq, prf)) = thinOccursInAnyInv' f i as occurs in
-      (j ** (eq, That prf)))
-    (\occurs1, occurs2 =>
-      let (j1 ** (eq1, prf1)) = thinOccursInInv' f i a occurs1 in
-      let (j2 ** (eq2, prf2)) = thinOccursInAnyInv' f i as occurs2 in
-      (j1 ** (eq1,
-        Both prf1 $
-        rewrite indexInjective f {x = j1, y = j2} $ trans eq1 (sym eq2) in
-        prf2)))
-
-thinOccursInInv :
-  (0 f : k `Thins` n) -> (0 i : Fin k) -> (a : Ty k) ->
-  index f i `OccursIn` thin f a ->
-  i `OccursIn` a
-thinOccursInInv f i a occurs =
-  let (j ** (eq, prf)) = thinOccursInInv' f (index f i) a occurs in
-  rewrite indexInjective f {x = i, y = j} $ sym eq in
-  prf
-
-thinOccursInAny1Inv :
-  (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List1 (Ty k)) ->
-  index f i `OccursInAny1` thinAll1 f as ->
-  i `OccursInAny1` as
-thinOccursInAny1Inv f i as occurs =
-  let (j ** (eq, prf)) = thinOccursInAny1Inv' f (index f i) as occurs in
-  rewrite indexInjective f {x = i, y = j} $ sym eq in
-  prf
-
--- Not Positive --
-
-thinNotPositiveInv :
-  (0 f : k `Thins` n) -> (0 i : Fin k) -> (a : Ty k) ->
-  index f i `NotPositiveIn` thin f a -> i `NotPositiveIn` a
-thinNotPositiveAnyInv :
-  (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List (Ty k)) ->
-  index f i `NotPositiveInAny` thinAll f as -> i `NotPositiveInAny` as
-thinNotPositiveAny1Inv :
-  (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List1 (Ty k)) ->
-  index f i `NotPositiveInAny1` thinAll1 f as -> i `NotPositiveInAny1` as
-
-thinNotPositiveInv f i (TVar j) = id
-thinNotPositiveInv f i TNat = id
-thinNotPositiveInv f i (TArrow a b) =
-  bimap
-    (thinOccursInInv f i a)
-    (thinNotPositiveInv f i b)
-thinNotPositiveInv f i (TUnion as) = thinNotPositiveAny1Inv f i as
-thinNotPositiveInv f i (TProd as) = thinNotPositiveAnyInv f i as
-thinNotPositiveInv f i (TSum as) = thinNotPositiveAnyInv f i as
-thinNotPositiveInv f i (TFix a) =
-  \occurs =>
-    thinOccursInInv (Keep f) (FS i) a $
-    rewrite indexKeepFS f i in
-    occurs
-
-thinNotPositiveAnyInv f i [] = id
-thinNotPositiveAnyInv f i (a :: as) =
-  bimap (thinNotPositiveInv f i a) (thinNotPositiveAnyInv f i as)
-
-thinNotPositiveAny1Inv f i (a ::: as) =
-  bimap (thinNotPositiveInv f i a) (thinNotPositiveAnyInv f i as)
-
--- Ill Formed --
-
-thinIllFormedInv :
-  (0 f : k `Thins` n) -> (a : Ty k) ->
-  IllFormed (thin f a) -> IllFormed a
-thinAnyIllFormedInv :
-  (0 f : k `Thins` n) -> (as : List (Ty k)) ->
-  AnyIllFormed (thinAll f as) -> AnyIllFormed as
-thinAny1IllFormedInv :
-  (0 f : k `Thins` n) -> (as : List1 (Ty k)) ->
-  Any1IllFormed (thinAll1 f as) -> Any1IllFormed as
-
-thinIllFormedInv f (TVar i) = id
-thinIllFormedInv f TNat = id
-thinIllFormedInv f (TArrow a b) = bimap (thinIllFormedInv f a) (thinIllFormedInv f b)
-thinIllFormedInv f (TUnion as) = thinAny1IllFormedInv f as
-thinIllFormedInv f (TProd as) = thinAnyIllFormedInv f as
-thinIllFormedInv f (TSum as) = thinAnyIllFormedInv f as
-thinIllFormedInv f (TFix a) =
-  bimap
-    (\npos => thinNotPositiveInv (Keep f) FZ a $ rewrite indexKeepFZ f in npos)
-    (thinIllFormedInv (Keep f) a)
-
-thinAnyIllFormedInv f [] = id
-thinAnyIllFormedInv f (a :: as) = bimap (thinIllFormedInv f a) (thinAnyIllFormedInv f as)
-
-thinAny1IllFormedInv f (a ::: as) = bimap (thinIllFormedInv f a) (thinAnyIllFormedInv f as)
-
---------------------------------------------------------------------------------
 -- Substitution ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 public export
-fromVar : Either (Fin n) (Ty n) -> Ty n
+fromVar : Either (Var ctx v) (Ty ctx v) -> Ty ctx v
 fromVar = either TVar id
 
 export
-sub : Env k n (Ty n) -> Ty k -> Ty n
-subAll : Env k n (Ty n) -> List (Ty k) -> List (Ty n)
-subAll1 : Env k n (Ty n) -> List1 (Ty k) -> List1 (Ty n)
+sub : Env ctx1 ctx2 (Ty ctx2) -> Ty ctx1 v -> Ty ctx2 v
+subAll : Env ctx1 ctx2 (Ty ctx2) -> Row (Ty ctx1 v) -> Row (Ty ctx2 v)
+subAllFresh :
+  (env : Env ctx1 ctx2 (Ty ctx2)) -> (x : String) ->
+  (row : Row (Ty ctx1 v)) ->
+  So (x `freshIn` row) -> So (x `freshIn` subAll env row)
 
 sub env (TVar i) = fromVar $ lookup env i
 sub env TNat = TNat
 sub env (TArrow a b) = TArrow (sub env a) (sub env b)
-sub env (TUnion as) = TUnion (subAll1 env as)
 sub env (TProd as) = TProd (subAll env as)
 sub env (TSum as) = TSum (subAll env as)
-sub env (TFix a) = TFix (sub (lift (Drop Id) env :< TVar FZ) a)
-
-subAll env [] = []
-subAll env (a :: as) = sub env a :: subAll env as
-
-subAll1 env (a ::: as) = sub env a ::: subAll env as
-
--- Properties ------------------------------------------------------------------
-
-pushEither :
-  (0 f : c -> d) -> (0 g : a -> c) -> (0 h : b -> c) -> (x : Either a b) ->
-  f (either g h x) = either (f . g) (f . h) x
-pushEither f g h (Left x) = Refl
-pushEither f g h (Right x) = Refl
-
--- Occurs --
-
-subOccursIn :
-  (env : Env k n (Ty n)) -> (i : Fin k) -> (a : Ty k) ->
-  j `OccursIn` fromVar (lookup env i) ->
-  i `OccursIn` a ->
-  j `OccursIn` sub env a
-subOccursInAny :
-  (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List (Ty k)) ->
-  j `OccursIn` fromVar (lookup env i) ->
-  i `OccursInAny` as ->
-  j `OccursInAny` subAll env as
-subOccursInAny1 :
-  (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List1 (Ty k)) ->
-  j `OccursIn` fromVar (lookup env i) ->
-  i `OccursInAny1` as ->
-  j `OccursInAny1` subAll1 env as
-
-subOccursIn env i (TVar x) occurs = \Refl => occurs
-subOccursIn env i TNat occurs = id
-subOccursIn env i (TArrow a b) occurs =
-  bimap
-    (subOccursIn env i a occurs)
-    (subOccursIn env i b occurs)
-subOccursIn env i (TUnion as) occurs = subOccursInAny1 env i as occurs
-subOccursIn env i (TProd as) occurs = subOccursInAny env i as occurs
-subOccursIn env i (TSum as) occurs = subOccursInAny env i as occurs
-subOccursIn env i (TFix a) occurs =
-  subOccursIn (lift (Drop Id) env :< TVar FZ) (FS i) a {j = FS j} $
-    rewrite lookupFS (lift (Drop Id) env) (TVar FZ) i in
-    rewrite lookupLift (Drop Id) env i in
-    rewrite eitherBimapFusion TVar id (index (Drop Id)) (thin (Drop Id)) (lookup env i) in
-    rewrite sym $ pushEither (thin (Drop Id)) TVar id (lookup env i) in
-    rewrite sym $ indexId j in
-    rewrite sym $ indexDrop Id j in
-    thinOccursIn (Drop Id) j (fromVar $ lookup env i) $
-    occurs
-
-subOccursInAny env i [] occurs = id
-subOccursInAny env i (a :: as) occurs =
-  bimap (subOccursIn env i a occurs) (subOccursInAny env i as occurs)
-
-subOccursInAny1 env i (a ::: as) occurs =
-  bimap (subOccursIn env i a occurs) (subOccursInAny env i as occurs)
-
--- Inverse
-
-0 EnvOccursUniq : Env k n (Ty n) -> (i : Fin n) -> (j : Fin k) -> Type
-EnvOccursUniq env i j = (x : Fin k) -> i `OccursIn` fromVar (lookup env x) -> j = x
-
-liftEnvOccursUniq :
-  (0 env : Env k n (Ty n)) ->
-  EnvOccursUniq env i j ->
-  EnvOccursUniq (lift (Drop Id) env :< TVar FZ) (FS i) (FS j)
-liftEnvOccursUniq env prf FZ =
-  rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in
-  absurd
-liftEnvOccursUniq env prf (FS x) =
-  rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in
-  rewrite lookupLift (Drop Id) env x in
-  rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in
-  \occurs =>
-  cong FS $
-  prf x $
-  thinOccursInInv (Drop Id) i (fromVar $ lookup env x) $
-  rewrite pushEither (rename (Drop Id)) TVar id (lookup env x) in
-  rewrite indexDrop Id i in
-  rewrite indexId i in
-  occurs
-
-liftOccursUniqFZ :
-  (env : Env k n (Ty n)) ->
-  EnvOccursUniq (lift (Drop Id) env :< TVar FZ) FZ FZ
-liftOccursUniqFZ env FZ =
-  rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in
-  const Refl
-liftOccursUniqFZ env (FS x) =
-  rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in
-  rewrite lookupLift (Drop Id) env x in
-  rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in
-  \occurs =>
-  let
-    (j ** (eq, occurs')) =
-      thinOccursInInv' (Drop Id) FZ (fromVar $ lookup env x) $
-      rewrite pushEither (rename (Drop Id)) TVar id (lookup env x) in
-      occurs
-  in
-  absurd $ trans (sym eq) (indexDrop Id j)
-
-subOccursInInv :
-  (0 env : Env k n (Ty n)) ->
-  (0 prf : EnvOccursUniq env i j) ->
-  (a : Ty k) ->
-  i `OccursIn` sub env a -> j `OccursIn` a
-subOccursInAnyInv :
-  (0 env : Env k n (Ty n)) ->
-  (0 prf : EnvOccursUniq env i j) ->
-  (as : List (Ty k)) ->
-  i `OccursInAny` subAll env as -> j `OccursInAny` as
-subOccursInAny1Inv :
-  (0 env : Env k n (Ty n)) ->
-  (0 prf : EnvOccursUniq env i j) ->
-  (as : List1 (Ty k)) ->
-  i `OccursInAny1` subAll1 env as -> j `OccursInAny1` as
-
-subOccursInInv env prf (TVar x) = \p => irrelevantEq $ prf x p
-subOccursInInv env prf TNat = id
-subOccursInInv env prf (TArrow a b) =
-  bimap
-    (subOccursInInv env prf a)
-    (subOccursInInv env prf b)
-subOccursInInv env prf (TUnion as) = subOccursInAny1Inv env prf as
-subOccursInInv env prf (TProd as) = subOccursInAnyInv env prf as
-subOccursInInv env prf (TSum as) = subOccursInAnyInv env prf as
-subOccursInInv env prf (TFix a) =
-  subOccursInInv
-    (lift (Drop Id) env :< TVar FZ)
-    (liftEnvOccursUniq env prf)
-    a
-
-subOccursInAnyInv env prf [] = id
-subOccursInAnyInv env prf (a :: as) =
-  bimap
-    (subOccursInInv env prf a)
-    (subOccursInAnyInv env prf as)
-
-subOccursInAny1Inv env prf (a ::: as) =
-  bimap
-    (subOccursInInv env prf a)
-    (subOccursInAnyInv env prf as)
-
-
--- Not Positive --
-
-subNotPositiveIn :
-  (env : Env k n (Ty n)) -> (i : Fin k) -> (a : Ty k) ->
-  j `OccursIn` fromVar (lookup env i) ->
-  i `NotPositiveIn` a ->
-  j `NotPositiveIn` sub env a
-subNotPositiveInAny :
-  (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List (Ty k)) ->
-  j `OccursIn` fromVar (lookup env i) ->
-  i `NotPositiveInAny` as ->
-  j `NotPositiveInAny` subAll env as
-subNotPositiveInAny1 :
-  (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List1 (Ty k)) ->
-  j `OccursIn` fromVar (lookup env i) ->
-  i `NotPositiveInAny1` as ->
-  j `NotPositiveInAny1` subAll1 env as
-
-subNotPositiveIn env i (TVar x) occurs = absurd
-subNotPositiveIn env i TNat occurs = id
-subNotPositiveIn env i (TArrow a b) occurs =
-  bimap
-    (subOccursIn env i a occurs)
-    (subNotPositiveIn env i b occurs)
-subNotPositiveIn env i (TUnion as) occurs = subNotPositiveInAny1 env i as occurs
-subNotPositiveIn env i (TProd as) occurs = subNotPositiveInAny env i as occurs
-subNotPositiveIn env i (TSum as) occurs = subNotPositiveInAny env i as occurs
-subNotPositiveIn env i (TFix a) occurs =
-  subOccursIn (lift (Drop Id) env :< TVar FZ) (FS i) a {j = FS j} $
-    rewrite lookupFS (lift (Drop Id) env) (TVar FZ) i in
-    rewrite lookupLift (Drop Id) env i in
-    rewrite eitherBimapFusion TVar id (index (Drop Id)) (thin (Drop Id)) (lookup env i) in
-    rewrite sym $ pushEither (thin (Drop Id)) TVar id (lookup env i) in
-    rewrite sym $ indexId j in
-    rewrite sym $ indexDrop Id j in
-    thinOccursIn (Drop Id) j (fromVar $ lookup env i) $
-    occurs
-
-subNotPositiveInAny env i [] occurs = id
-subNotPositiveInAny env i (a :: as) occurs =
-  bimap
-    (subNotPositiveIn env i a occurs)
-    (subNotPositiveInAny env i as occurs)
-
-subNotPositiveInAny1 env i (a ::: as) occurs =
-  bimap
-    (subNotPositiveIn env i a occurs)
-    (subNotPositiveInAny env i as occurs)
-
--- Inverse
-
-0 EnvPositiveIn : Env k n (Ty n) -> (i : Fin n) -> Type
-EnvPositiveIn env i = (x : Fin k) -> Not (i `NotPositiveIn` fromVar (lookup env x))
-
-liftPositiveInFZ :
-  (env : Env k n (Ty n)) ->
-  EnvPositiveIn (lift (Drop Id) env :< TVar FZ) FZ
-liftPositiveInFZ env FZ =
-  rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in
-  id
-liftPositiveInFZ env (FS x) =
-  rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in
-  rewrite lookupLift (Drop Id) env x in
-  rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in
-  \npos =>
-  let
-    (j ** (eq, occurs)) =
-      thinOccursInInv' (Drop Id) FZ (fromVar $ lookup env x) $
-      rewrite pushEither (thin (Drop Id)) TVar id (lookup env x) in
-      notPositiveToOccurs _ npos
-  in
-  absurd $ trans (sym (indexDrop Id j)) eq
-
-subNotPositiveInInv :
-  (0 env : Env k n (Ty n)) ->
-  (0 prf1 : EnvPositiveIn env i) ->
-  (0 prf2 : EnvOccursUniq env i j) ->
-  (a : Ty k) ->
-  i `NotPositiveIn` sub env a -> j `NotPositiveIn` a
-subNotPositiveInAnyInv :
-  (0 env : Env k n (Ty n)) ->
-  (0 prf1 : EnvPositiveIn env i) ->
-  (0 prf2 : EnvOccursUniq env i j) ->
-  (as : List (Ty k)) ->
-  i `NotPositiveInAny` subAll env as -> j `NotPositiveInAny` as
-subNotPositiveInAny1Inv :
-  (0 env : Env k n (Ty n)) ->
-  (0 prf1 : EnvPositiveIn env i) ->
-  (0 prf2 : EnvOccursUniq env i j) ->
-  (as : List1 (Ty k)) ->
-  i `NotPositiveInAny1` subAll1 env as -> j `NotPositiveInAny1` as
-
-subNotPositiveInInv env prf1 prf2 (TVar x) = \npos => void $ prf1 x npos
-subNotPositiveInInv env prf1 prf2 TNat = id
-subNotPositiveInInv env prf1 prf2 (TArrow a b) =
-  bimap
-    (subOccursInInv env prf2 a)
-    (subNotPositiveInInv env prf1 prf2 b)
-subNotPositiveInInv env prf1 prf2 (TUnion as) = subNotPositiveInAny1Inv env prf1 prf2 as
-subNotPositiveInInv env prf1 prf2 (TProd as) = subNotPositiveInAnyInv env prf1 prf2 as
-subNotPositiveInInv env prf1 prf2 (TSum as) = subNotPositiveInAnyInv env prf1 prf2 as
-subNotPositiveInInv env prf1 prf2 (TFix a) =
-  subOccursInInv
-    (lift (Drop Id) env :< TVar FZ)
-    (liftEnvOccursUniq env prf2)
-    a
-
-subNotPositiveInAnyInv env prf1 prf2 [] = id
-subNotPositiveInAnyInv env prf1 prf2 (a :: as) =
-  bimap
-    (subNotPositiveInInv env prf1 prf2 a)
-    (subNotPositiveInAnyInv env prf1 prf2 as)
-
-subNotPositiveInAny1Inv env prf1 prf2 (a ::: as) =
-  bimap
-    (subNotPositiveInInv env prf1 prf2 a)
-    (subNotPositiveInAnyInv env prf1 prf2 as)
-
--- Ill Formed --
-
-subIllFormed :
-  (env : Env k n (Ty n)) -> (a : Ty k) ->
-  IllFormed a -> IllFormed (sub env a)
-subAnyIllFormed :
-  (env : Env k n (Ty n)) -> (as : List (Ty k)) ->
-  AnyIllFormed as -> AnyIllFormed (subAll env as)
-subAny1IllFormed :
-  (env : Env k n (Ty n)) -> (as : List1 (Ty k)) ->
-  Any1IllFormed as -> Any1IllFormed (subAll1 env as)
-
-subIllFormed env (TVar i) = absurd
-subIllFormed env TNat = id
-subIllFormed env (TArrow a b) = bimap (subIllFormed env a) (subIllFormed env b)
-subIllFormed env (TUnion as) = subAny1IllFormed env as
-subIllFormed env (TProd as) = subAnyIllFormed env as
-subIllFormed env (TSum as) = subAnyIllFormed env as
-subIllFormed env (TFix a) =
-  bimap
-    (subNotPositiveIn (lift (Drop Id) env :< TVar FZ) FZ a $
-      rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in
-      Refl)
-    (subIllFormed (lift (Drop Id) env :< TVar FZ) a)
-
-subAnyIllFormed env [] = id
-subAnyIllFormed env (a :: as) = bimap (subIllFormed env a) (subAnyIllFormed env as)
-
-subAny1IllFormed env (a ::: as) = bimap (subIllFormed env a) (subAnyIllFormed env as)
-
--- Inverse
+sub env (TFix x a) = TFix x (sub (lift (Drop Id) env :< (x :- TVar (%% x))) a)
 
-export
-0 EnvWellFormed : Env k n (Ty n) -> Type
-EnvWellFormed env = (x : Fin k) -> Not (IllFormed $ fromVar $ lookup env x)
-
-liftEnvWellFormed :
-  (env : Env k n (Ty n)) ->
-  EnvWellFormed env ->
-  EnvWellFormed (lift (Drop Id) env :< TVar FZ)
-liftEnvWellFormed env prf FZ =
-  rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in
-  id
-liftEnvWellFormed env prf (FS x) =
-  rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in
-  rewrite lookupLift (Drop Id) env x in
-  rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in
-  \ill =>
-  prf x $
-  thinIllFormedInv (Drop Id) (either TVar id $ lookup env x) $
-  rewrite pushEither (thin (Drop Id)) TVar id (lookup env x) in
-  ill
-
-subIllFormedInv :
-  (0 env : Env k n (Ty n)) ->
-  (0 prf : EnvWellFormed env) ->
-  (a : Ty k) ->
-  IllFormed (sub env a) -> IllFormed a
-subAnyIllFormedInv :
-  (0 env : Env k n (Ty n)) ->
-  (0 prf : EnvWellFormed env) ->
-  (as : List (Ty k)) ->
-  AnyIllFormed (subAll env as) -> AnyIllFormed as
-subAny1IllFormedInv :
-  (0 env : Env k n (Ty n)) ->
-  (0 prf : EnvWellFormed env) ->
-  (as : List1 (Ty k)) ->
-  Any1IllFormed (subAll1 env as) -> Any1IllFormed as
-
-subIllFormedInv env prf (TVar i) = \ill => void $ prf i ill
-subIllFormedInv env prf TNat = id
-subIllFormedInv env prf (TArrow a b) =
-  bimap
-    (subIllFormedInv env prf a)
-    (subIllFormedInv env prf b)
-subIllFormedInv env prf (TUnion as) = subAny1IllFormedInv env prf as
-subIllFormedInv env prf (TProd as) = subAnyIllFormedInv env prf as
-subIllFormedInv env prf (TSum as) = subAnyIllFormedInv env prf as
-subIllFormedInv env prf (TFix a) =
-  bimap
-    (subNotPositiveInInv
-      (lift (Drop Id) env :< TVar FZ)
-      (liftPositiveInFZ env)
-      (liftOccursUniqFZ env)
-      a)
-    (subIllFormedInv
-      (lift (Drop Id) env :< TVar FZ)
-      (liftEnvWellFormed env prf)
-      a)
-
-subAnyIllFormedInv env prf [] = id
-subAnyIllFormedInv env prf (a :: as) =
-  bimap
-    (subIllFormedInv env prf a)
-    (subAnyIllFormedInv env prf as)
-
-subAny1IllFormedInv env prf (a ::: as) =
-  bimap
-    (subIllFormedInv env prf a)
-    (subAnyIllFormedInv env prf as)
-
--- Equivalent
+subAll env [<] = [<]
+subAll env ((:<) as (x :- a) {fresh}) =
+  (:<) (subAll env as) (x :- sub env a) {fresh = subAllFresh env x as fresh}
 
-export
-subIllFormedEquiv :
-  (env : Env k n (Ty n)) ->
-  (0 prf : EnvWellFormed env) ->
-  (a : Ty k) ->
-  IllFormed a <=> IllFormed (sub env a)
-subIllFormedEquiv env prf a =
-  MkEquivalence
-    { leftToRight = subIllFormed env a
-    , rightToLeft = subIllFormedInv env prf a
-    }
+subAllFresh env x [<] = id
+subAllFresh env x (as :< (y :- a)) = andSo . mapSnd (subAllFresh env x as) . soAnd
diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index 074d86e..1f2d35b 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -1,73 +1,43 @@
 module Inky.Type.Pretty
 
-import Data.Fin
-import Data.Fin.Extra
-import Data.List
-import Data.String
+import Inky.Context
 import Inky.Type
 import Text.PrettyPrint.Prettyprinter
 
-asTyChar : Fin 6 -> Char
-asTyChar = index' ['X', 'Y', 'Z', 'A', 'B', 'C']
-
-export
-typeName : Nat -> String
-typeName n with (divMod n 6)
-  typeName _ | Fraction _ 6 q r Refl =
-    strSnoc
-      (if q == 0 then "'" else assert_total (typeName $ pred q))
-      (asTyChar r)
-
-arrowPrec, unionPrec, prodPrec, sumPrec, fixPrec : Prec
+arrowPrec, prodPrec, sumPrec, fixPrec : Prec
 arrowPrec = Open
-unionPrec = User 2
 prodPrec = Open
-sumPrec = User 1
+sumPrec = Open
 fixPrec = Open
 
 export
-prettyType : {ty : Nat} -> Ty ty -> Prec -> Doc ann
-prettyTypeAll : {ty : Nat} -> List (Ty ty) -> Prec -> List (Doc ann)
-prettyTypeAll1 : {ty : Nat} -> List1 (Ty ty) -> Prec -> List (Doc ann)
+prettyType : {ctx : Context ()} -> Ty ctx () -> Prec -> Doc ann
+prettyTypeRow : {ctx : Context ()} -> Row (Ty ctx ()) -> Prec -> List (Doc ann)
 
-prettyType (TVar i) d = pretty (typeName $ finToNat i)
+prettyType (TVar i) d = pretty (unVal $ nameOf i)
 prettyType TNat d = pretty "Nat"
 prettyType (TArrow a b) d =
   parenthesise (d > arrowPrec) $ group $ align $ hang 2 $
     let parts = stripArrow b in
-    concatWith (\x, y => x <++> "->" <+> line <+> y) (prettyType a arrowPrec :: parts)
+    concatWith (surround $ "->" <+> line) (prettyType a arrowPrec :: parts)
   where
-  stripArrow : Ty ty -> List (Doc ann)
+  stripArrow : Ty ctx () -> List (Doc ann)
   stripArrow (TArrow a b) = prettyType a arrowPrec :: stripArrow b
   stripArrow a = [prettyType a arrowPrec]
-prettyType (TUnion (a ::: [])) d =
-  parens $ group $ align $ hang 2 $
-    prettyType a unionPrec <++> "&"
-prettyType (TUnion as) d =
-  parenthesise (d >= unionPrec) $ group $ align $ hang 2 $
-    let parts = prettyTypeAll1 as unionPrec in
-    concatWith (\x, y => x <++> "&" <+> line <+> y) parts
-prettyType (TProd [a]) d =
-  parens $ group $ align $ hang 2 $
-    prettyType a prodPrec <++> ","
 prettyType (TProd as) d =
-  parens $ group $ align $ hang 2 $
-    let parts = prettyTypeAll as prodPrec in
-    concatWith (\x, y => x <++> "," <+> line <+> y) parts
-prettyType (TSum []) d = "(+)"
-prettyType (TSum [a]) d =
-  parens $ group $ align $ hang 2 $
-    prettyType a sumPrec <++> "+"
+  enclose "<" ">" $ group $ align $ hang 2 $
+    let parts = prettyTypeRow as prodPrec in
+    concatWith (surround $ "," <+> line) parts
 prettyType (TSum as) d =
-  parenthesise (d >= sumPrec) $ group $ align $ hang 2 $
-    let parts = prettyTypeAll as sumPrec in
-    concatWith (\x, y => x <++> "+" <+> line <+> y) parts
-prettyType (TFix a) d =
+  enclose "[" "]" $ group $ align $ hang 2 $
+    let parts = prettyTypeRow as prodPrec in
+    concatWith (surround $ "," <+> line) parts
+prettyType (TFix x a) d =
   parens $ group $ align $ hang 2 $
-    "\\" <+> pretty (typeName ty) <++> "=>" <+> line <+>
+    "\\" <+> pretty x <++> "=>" <+> line <+>
     prettyType a fixPrec
 
-prettyTypeAll [] d = []
-prettyTypeAll (a :: as) d = prettyType a d :: prettyTypeAll as d
-
-prettyTypeAll1 (a ::: as) d = prettyType a d :: prettyTypeAll as d
+prettyTypeRow [<] d = []
+prettyTypeRow (as :< (x :- a)) d =
+  (group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyType a d)
+  :: prettyTypeRow as d