diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,19 @@
 Changelog
 =========
 
+Version 0.1.2.0
+---------------
+
+*August 12, 2019*
+
+<https://github.com/mstksg/list-witnesses/releases/tag/v0.1.2.0>
+
+*   Add predicates (`IsInsert`, `IsPrefix`, etc.) and `Auto` and `Decidable`
+    instances for most of the data types, for auto-generation and searches.
+*   Add some functions for creating `Append`s and witnesses of concatenation
+    type families from `Append`s.
+*   `interleavedIxes`, for more manipulation of `Interleave`
+
 Version 0.1.1.1
 ---------------
 
diff --git a/list-witnesses.cabal b/list-witnesses.cabal
--- a/list-witnesses.cabal
+++ b/list-witnesses.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: a6892eb45e6aae7a7e7c3f4b23c95bdd2299a3a95a190137567cd326e5045529
+-- hash: 7abc29a51e67cb59dca3b968d5864b7bcfd1126df6a3bb4166c3eddd2999129f
 
 name:           list-witnesses
-version:        0.1.1.1
+version:        0.1.2.0
 synopsis:       Witnesses for working with type-level lists
 description:    Collection of assorted inductive witnesses and functions for working with
                 type-level lists.
@@ -24,7 +24,7 @@
 copyright:      (c) Justin Le 2018
 license:        BSD3
 license-file:   LICENSE
-tested-with:    GHC >= 8.4
+tested-with:    GHC >= 8.6
 build-type:     Simple
 extra-source-files:
     README.md
@@ -45,7 +45,8 @@
   ghc-options: -Wall -Wcompat -Wredundant-constraints -Werror=incomplete-patterns
   build-depends:
       base >=4.7 && <5
-    , decidable >=0.1.5
+    , decidable >=0.2
+    , functor-products
     , microlens
     , profunctors
     , singletons
diff --git a/src/Data/Type/List/Edit.hs b/src/Data/Type/List/Edit.hs
--- a/src/Data/Type/List/Edit.hs
+++ b/src/Data/Type/List/Edit.hs
@@ -1,14 +1,19 @@
-{-# LANGUAGE EmptyCase            #-}
-{-# LANGUAGE GADTs                #-}
-{-# LANGUAGE KindSignatures       #-}
-{-# LANGUAGE LambdaCase           #-}
-{-# LANGUAGE RankNTypes           #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE StandaloneDeriving   #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE TypeInType           #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE EmptyCase             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeInType            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 -- |
 -- Module      : Data.Type.List.Edit
@@ -22,13 +27,17 @@
 -- Witnesses regarding single-item edits of lists.
 module Data.Type.List.Edit (
   -- * Simple edits
-    Insert(..)
-  , Delete(..)
+    Insert(..), autoInsert
+  , Delete(..), autoDelete
   , insToDel
   , delToIns
-  , Substitute(..)
+  , Substitute(..), autoSubstitute
   , flipSub
   , subToDelIns
+  -- ** Predicates
+  , IsInsert, InsertedInto
+  , IsDelete, DeletedFrom
+  , IsSubstitute
   -- ** Singletons
   , SInsert(..)
   , SDelete(..)
@@ -61,10 +70,15 @@
 
 import           Data.Kind
 import           Data.Singletons
-import           Data.Type.Universe
-import           Data.Vinyl.Core
-import           Lens.Micro
-import qualified Control.Category      as C
+import           Data.Singletons.Decide
+import           Data.Singletons.Prelude
+import           Data.Singletons.Sigma
+import           Data.Type.Functor.Product
+import           Data.Type.Predicate
+import           Data.Type.Predicate.Auto
+import           Data.Type.Predicate.Param
+import           Lens.Micro hiding         ((%~))
+import qualified Control.Category          as C
 
 -- | An @'Insert' as bs x@ is a witness that you can insert @x@ into some
 -- position in list @as@ to produce list @bs@.  It is essentially 'Delete'
@@ -86,6 +100,94 @@
 
 deriving instance Show (Insert as bs x)
 
+-- | A type-level predicate that a given value can be used as an insertion
+-- to change @as@ to @bs@.
+--
+-- @since 0.1.2.0
+type IsInsert as bs = TyPred (Insert as bs)
+
+instance Auto (IsInsert as (x ': as)) x where
+    auto = InsZ
+
+instance Auto (IsInsert as bs) x => Auto (IsInsert (a ': as) (a ': bs)) x where
+    auto = InsS (auto @_ @(IsInsert as bs) @x)
+
+instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInsert as bs) where
+    decide z = case sing @bs of
+      SNil -> Disproved $ \case {}
+      y `SCons` (ys@Sing :: Sing bs') -> case y %~ z of
+        Proved Refl -> case sing @as %~ ys of
+          Proved Refl -> Proved InsZ
+          Disproved v -> case sing @as of
+            SNil -> Disproved $ \case
+              InsZ -> v Refl
+            x `SCons` (Sing :: Sing as') -> case x %~ y of
+              Proved Refl -> case decide @(IsInsert as' bs') z of
+                Proved i -> Proved $ InsS i
+                Disproved u -> Disproved $ \case
+                  InsZ -> u InsZ
+                  InsS i -> u i
+              Disproved u -> Disproved $ \case
+                InsZ   -> v Refl
+                InsS _ -> u Refl
+        Disproved v -> case sing @as of
+          SNil -> Disproved $ \case
+            InsZ -> v Refl
+          x `SCons` (Sing :: Sing as') -> case x %~ y of
+            Proved Refl -> case decide @(IsInsert as' bs') z of
+              Proved i -> Proved $ InsS i
+              Disproved u -> Disproved $ \case
+                InsZ -> u InsZ
+                InsS i -> u i
+            Disproved u -> Disproved $ \case
+              InsZ   -> v Refl
+              InsS _ -> u Refl
+
+-- | If @bs@ satisfies @'InsertedInto' as@, it means that there exists some
+-- element @x@ such that @'IsInsert' as bs \@\@ x@: you can get @bs@ by
+-- inserting @x@ into @as@ somewhere.
+--
+-- In other words, @'InsertedInto' as@ is satisfied by @bs@ if you can turn
+-- @as@ into @bs@ by inserting one individual item.
+--
+-- You can find this element (if it exists) using 'search', or the
+-- 'Decidable' instance of @'Found' ('InsertedInto' as)@:
+--
+-- @
+-- 'searchTC' :: SingI as => Sing bs -> 'Decision' ('Σ' k ('IsInsert' as bs))
+-- @
+--
+-- This will find you the single element you need to insert into @as@ to
+-- get @bs@, if it exists.
+--
+-- @since 0.1.2.0
+type InsertedInto (as :: [k]) = (TyPP (Insert as) :: ParamPred [k] k)
+
+instance (SDecide k, SingI (as :: [k])) => Decidable (Found (InsertedInto as)) where
+    decide = \case
+      SNil -> Disproved $ \(_ :&: i) -> case i of {}
+      y `SCons` ys -> case sing @as %~ ys of
+        Proved Refl -> Proved $ y :&: InsZ
+        Disproved v -> case sing @as of
+          SNil -> Disproved $ \(_ :&: i) -> case i of
+            InsZ -> v Refl
+          x `SCons` (Sing :: Sing as') -> case x %~ y of
+            Proved Refl -> case decide @(Found (InsertedInto as')) ys of
+              Proved (z :&: i) -> Proved $ z :&: InsS i
+              Disproved u      -> Disproved $ \(z :&: i) -> case i of
+                InsZ    -> u $ z :&: InsZ
+                InsS i' -> u $ z :&: i'
+            Disproved u -> Disproved $ \(_ :&: i) -> case i of
+              InsZ   -> v Refl
+              InsS _ -> u Refl
+
+-- | Automatically generate an 'Insert' if @as@, @bs@ and @x@ are known
+-- statically.
+--
+-- @since 0.1.2.0
+autoInsert :: forall as bs x. Auto (IsInsert as bs) x => Insert as bs x
+autoInsert = auto @_ @(IsInsert as bs) @x
+
 -- | Kind-indexed singleton for 'Insert'.
 data SInsert as bs x :: Insert as bs x -> Type where
     SInsZ :: SInsert as (x ': as) x 'InsZ
@@ -117,6 +219,54 @@
 
 deriving instance Show (Delete as bs x)
 
+-- | A type-level predicate that a given value can be used as a deletion
+-- to change @as@ to @bs@.
+--
+-- @since 0.1.2.0
+type IsDelete as bs = TyPred (Delete as bs)
+
+instance Auto (IsDelete (x ': as) as) x where
+    auto = DelZ
+
+instance Auto (IsDelete as bs) x => Auto (IsDelete (a ': as) (a ': bs)) x where
+    auto = DelS (auto @_ @(IsDelete as bs) @x)
+
+instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsDelete as bs) where
+    decide = mapDecision insToDel delToIns . decide @(IsInsert bs as)
+
+-- | If @bs@ satisfies @'DeletedFrom' as@, it means that there exists some
+-- element @x@ such that @'IsDelete' as bs \@\@ x@: you can get @bs@ by
+-- deleting @x@ from @as@ somewhere.
+--
+-- In other words, @'DeletedFrom' as@ is satisfied by @bs@ if you can turn
+-- @as@ into @bs@ by deleting one individual item.
+--
+-- You can find this element (if it exists) using 'search', or the
+-- 'Decidable' instance of @'Found' ('DeletedFrom' as)@.
+--
+-- @
+-- 'searchTC' :: SingI as => Sing bs -> 'Decision' ('Σ' k ('IsDelete' as bs))
+-- @
+--
+-- This will find you the single element you need to delete from @as@ to
+-- get @bs@, if it exists.
+--
+-- @since 0.1.2.0
+type DeletedFrom (as :: [k]) = (TyPP (Delete as) :: ParamPred [k] k)
+
+instance (SDecide k, SingI (as :: [k])) => Decidable (Found (DeletedFrom as)) where
+    decide (Sing :: Sing bs) =
+        mapDecision (mapSigma (sing @IdSym0) insToDel)
+                    (mapSigma (sing @IdSym0) delToIns)
+      $ decide @(Found (InsertedInto bs)) (sing @as)
+
+-- | Automatically generate an 'Delete' if @as@, @bs@ and @x@ are known
+-- statically.
+--
+-- @since 0.1.2.0
+autoDelete :: forall as bs x. Auto (IsDelete as bs) x => Delete as bs x
+autoDelete = auto @_ @(IsDelete as bs) @x
+
 -- | Kind-indexed singleton for 'Delete'.
 data SDelete as bs x :: Delete as bs x -> Type where
     SDelZ :: SDelete (x ': as) as x 'DelZ
@@ -147,6 +297,26 @@
 
 deriving instance Show (Substitute as bs x y)
 
+-- | A type-level predicate that a given value can be used as
+-- a substitution of @x@ to change @as@ to @bs@.
+--
+-- @since 0.1.2.0
+type IsSubstitute as bs x = TyPred (Substitute as bs x)
+
+instance Auto (IsSubstitute (x ': as) (y ': as) x) y where
+    auto = SubZ
+
+instance Auto (IsSubstitute as bs x) y => Auto (IsSubstitute (c ': as) (c ': bs) x) y where
+    auto = SubS (auto @_ @(IsSubstitute as bs x) @y)
+
+-- | Automatically generate an 'Substitute' if @as@, @bs@, @x@, and @y@ are
+-- known statically.
+--
+-- @since 0.1.2.0
+autoSubstitute :: forall as bs x y. Auto (IsSubstitute as bs x) y => Substitute as bs x y
+autoSubstitute = auto @_ @(IsSubstitute as bs x) @y
+
+
 -- | Kind-indexed singleton for 'Substitute'.
 data SSubstitute as bs x y :: Substitute as bs x y -> Type where
     SSubZ :: SSubstitute (x ': as) (y ': as) x y 'SubZ
@@ -193,7 +363,8 @@
     id = ENil
     xs . ys = compEdit ys xs
 
--- | Reverse an 'Edit' script.  O(n^2).  Please do not use.
+-- | Reverse an 'Edit' script.  O(n^2).  Please do not use ever in any
+-- circumstance.
 --
 -- TODO: Make O(n) using diff lists.
 flipEdit :: Edit as bs -> Edit bs as
@@ -241,8 +412,8 @@
 -- The number of 'SubS' in the index essentially indicates the index to
 -- edit at.
 --
--- This is similar to 'rlensC' from /vinyl/, but is built explicitly and
--- inductively, instead of using typeclass magic.
+-- This is similar to 'Data.Vinyl.Lens.rlensC' from /vinyl/, but is built
+-- explicitly and inductively, instead of using typeclass magic.
 recLens
     :: forall as bs x y f. ()
     => Substitute as bs x y
@@ -472,9 +643,9 @@
     SuccSubstitutedIx b bs x y x ('GotSubbed i) = 'GotSubbed ('IS i)
     SuccSubstitutedIx b bs x y z ('NotSubbed i) = 'NotSubbed ('IS i)
 
--- | Type-level version of 'subsituteIndex'.  Because of how GADTs and type
--- families interact, the type-level lists and kinds of the insertion and
--- index must be provided.
+-- | Type-level version of 'substituteIndex'.  Because of how GADTs and
+-- type families interact, the type-level lists and kinds of the insertion
+-- and index must be provided.
 type family SubstituteIndex as bs x y z (s :: Substitute as bs x y) (i :: Index as z) :: SubstitutedIx bs x y z where
     SubstituteIndex (z ': as) (y ': as) z y z 'SubZ     'IZ     = 'GotSubbed 'IZ
     SubstituteIndex (x ': as) (y ': as) x y z 'SubZ     ('IS i) = 'NotSubbed ('IS i)
diff --git a/src/Data/Type/List/Sublist.hs b/src/Data/Type/List/Sublist.hs
--- a/src/Data/Type/List/Sublist.hs
+++ b/src/Data/Type/List/Sublist.hs
@@ -1,13 +1,19 @@
-{-# LANGUAGE EmptyCase           #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE LambdaCase          #-}
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving  #-}
-{-# LANGUAGE TupleSections       #-}
-{-# LANGUAGE TypeInType          #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE EmptyCase             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE TupleSections         #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeInType            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE ViewPatterns          #-}
 
 -- |
 -- Module      : Data.Type.List.Sublist
@@ -22,31 +28,53 @@
 module Data.Type.List.Sublist (
   -- * Prefix and Suffix
   -- ** Prefix
-    Prefix(..)
+    Prefix(..), IsPrefix, autoPrefix
   , takeRec, prefixLens, takeIndex, weakenIndex
   -- ** Suffix
-  , Suffix(..)
+  , Suffix(..), IsSuffix, autoSuffix
   , dropRec, suffixLens, dropIndex, shiftIndex
   -- * Append
-  , Append(..)
+  , Append(..), IsAppend, autoAppend, withAppend
   , prefixToAppend, suffixToAppend
   , appendToPrefix, appendToSuffix, splitAppend
   -- ** Application
   , splitRec, appendRec, splitRecIso
   , splitIndex
+  -- ** Witnesses
+  -- *** Singletons
+  , pattern AppendWit
+  , appendWit, implyAppend, unAppendWit
+  -- *** Vinyl
+  , pattern AppendWitV
+  , appendWitV, implyAppendV, unAppendWitV
+  -- *** Both
+  , pattern AppendWit'
+  , convertAppends
+  , AppendedTo
   -- * Interleave
-  , Interleave(..)
+  , Interleave(..), IsInterleave, autoInterleave
   , interleaveRec, unweaveRec, interleaveRecIso
   , injectIndexL, injectIndexR, unweaveIndex
+  , interleavedIxes
   ) where
 
 import           Data.Bifunctor
 import           Data.Kind
 import           Data.Profunctor
-import           Data.Type.Universe
-import           Data.Vinyl.Core
-import           Lens.Micro
+import           Data.Singletons
+import           Data.Singletons.Decide
+import           Data.Singletons.Prelude.List
+import           Data.Singletons.Sigma
+import           Data.Type.Functor.Product
+import           Data.Type.Predicate
+import           Data.Type.Predicate.Auto
+import           Data.Type.Predicate.Param
+import           Data.Vinyl hiding            ((:~:))
+import           GHC.Generics                 ((:+:)(..))
+import           Lens.Micro hiding            ((%~))
 import           Lens.Micro.Extras
+import qualified Data.Vinyl.Recursive         as VR
+import qualified Data.Vinyl.TypeLevel         as V
 
 -- | A @'Prefix' as bs@ witnesses that @as@ is a prefix of @bs@.
 --
@@ -78,6 +106,37 @@
 takeRec :: Prefix as bs -> Rec f bs -> Rec f as
 takeRec p = view (prefixLens p)
 
+-- | A type-level predicate that a given list has @as@ as a prefix.
+--
+-- @since 0.1.2.0
+type IsPrefix as = TyPred (Prefix as)
+
+instance Auto (IsPrefix '[]) bs where
+    auto = PreZ
+
+instance Auto (IsPrefix as) bs => Auto (IsPrefix (a ': as)) (a ': bs) where
+    auto = PreS (auto @_ @(IsPrefix as) @bs)
+
+instance (SDecide k, SingI (as :: [k])) => Decidable (IsPrefix as) where
+    decide = case sing @as of
+      SNil         -> \_ -> Proved PreZ
+      x `SCons` (Sing :: Sing as') -> \case
+        SNil -> Disproved $ \case {}
+        y `SCons` (ys :: Sing bs') -> case x %~ y of
+          Proved Refl -> case decide @(IsPrefix as') ys of
+            Proved p -> Proved (PreS p)
+            Disproved v -> Disproved $ \case
+              PreS p -> v p
+          Disproved v -> Disproved $ \case
+            PreS _ -> v Refl
+
+-- | Automatically generate a 'Prefix' if @as@ and @bs@ are known
+-- statically.
+--
+-- @since 0.1.2.0
+autoPrefix :: forall as bs. Auto (IsPrefix as) bs => Prefix as bs
+autoPrefix = auto @_ @(IsPrefix as) @bs
+
 -- | A @'Suffix' as bs@ witnesses that @as@ is a suffix of @bs@.
 --
 -- Some examples:
@@ -100,6 +159,35 @@
 
 deriving instance Show (Suffix as bs)
 
+-- | A type-level predicate that a given list has @as@ as a suffix.
+--
+-- @since 0.1.2.0
+type IsSuffix as = TyPred (Suffix as)
+
+instance Auto (IsSuffix as) as where
+    auto = SufZ
+
+instance Auto (IsSuffix as) bs => Auto (IsSuffix as) (b ': bs) where
+    auto = SufS (auto @_ @(IsSuffix as) @bs)
+
+instance (SDecide k, SingI (as :: [k])) => Decidable (IsSuffix as) where
+    decide = \case
+      SNil -> case sing @as of
+        SNil -> Proved SufZ
+        _ `SCons` _ -> Disproved $ \case {}
+      _ `SCons` ys -> case decide @(IsSuffix as) ys of
+        Proved s    -> Proved $ SufS s
+        Disproved v -> Disproved $ \case
+          SufZ   -> error "help me"
+          SufS s -> v s
+
+-- | Automatically generate a 'Suffix' if @as@ and @bs@ are known
+-- statically.
+--
+-- @since 0.1.2.0
+autoSuffix :: forall as bs. Auto (IsSuffix as) bs => Suffix as bs
+autoSuffix = auto @_ @(IsSuffix as) @bs
+
 -- | A lens into the suffix of a 'Rec'.
 suffixLens :: Suffix as bs -> Lens' (Rec f bs) (Rec f as)
 suffixLens p = suffixToAppend p $ \a -> splitRecIso a . _2
@@ -129,6 +217,181 @@
 
 deriving instance Show (Append as bs cs)
 
+-- | A type-level predicate that a given list is the result of appending of
+-- @as@ and @bs@.
+--
+-- @since 0.1.2.0
+type IsAppend as bs = TyPred (Append as bs)
+
+-- | A parameterized predicate that you can use with 'select': With an
+-- @'AppendedTo' as@, you can give @bs@ and get @cs@ in return, where @cs@
+-- is the appending of @as@ and @bs@.
+--
+-- Run it with:
+--
+-- @
+-- 'selectTC' :: SingI as => Sing bs -> 'Σ' [k] ('IsAppend' as bs)
+-- @
+--
+-- 'select' for 'AppendedTo' is pretty much just 'withAppend'.
+--
+-- @since 0.1.2.0
+type AppendedTo as = TyPP (Append as)
+
+instance Auto (IsAppend '[] as) as where
+    auto = AppZ
+
+instance Auto (IsAppend as bs) cs => Auto (IsAppend (a ': as) bs) (a ': cs) where
+    auto = AppS (auto @_ @(IsAppend as bs) @cs)
+
+instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsAppend as bs) where
+    decide = case sing @as of
+      SNil         -> \cs -> case sing @bs %~ cs of
+        Proved Refl -> Proved AppZ
+        Disproved v -> Disproved $ \case
+          AppZ -> v Refl
+      x `SCons` (Sing :: Sing as') -> \case
+        SNil -> Disproved $ \case {}
+        y `SCons` (ys :: Sing bs') -> case x %~ y of
+          Proved Refl -> case decide @(IsAppend as' bs) ys of
+            Proved p -> Proved (AppS p)
+            Disproved v -> Disproved $ \case
+              AppS p -> v p
+          Disproved v -> Disproved $ \case
+            AppS _ -> v Refl
+
+instance SingI as => Decidable (Found (AppendedTo as))
+instance SingI as => Provable (Found (AppendedTo as)) where
+    prove ys = withAppend (singProd (sing @as)) (singProd ys) $ \s x -> prodSing s :&: x
+
+-- | Automatically generate an 'Append' if @as@, @bs@ and @cs@ are known
+-- statically.
+--
+-- @since 0.1.2.0
+autoAppend :: forall as bs cs. Auto (IsAppend as bs) cs => Append as bs cs
+autoAppend = auto @_ @(IsAppend as bs) @cs
+
+-- | Witness that @'Append' as bs cs@ implies @(as ++ bs) ~ cs@, using
+-- @++@ from "Data.Singletons.Prelude.List".
+--
+-- @since 0.1.2.0
+appendWit :: Append as bs cs -> (as ++ bs) :~: cs
+appendWit = \case
+    AppZ   -> Refl
+    AppS a -> case appendWit a of
+      Refl -> Refl
+
+-- | The inverse of 'appendWit': if we know @(as ++ bs) ~ cs@ (using @++@
+-- from "Data.Singletons.Prelude.List"), we can create an @'Append' as bs
+-- cs@ given structure witnesses 'Sing'.
+--
+-- @since 0.1.2.0
+unAppendWit
+    :: (as ++ bs) ~ cs
+    => Rec f as
+    -> Rec f bs
+    -> Append as bs cs
+unAppendWit = \case
+    RNil    -> \_   -> AppZ
+    _ :& xs -> AppS . unAppendWit xs
+
+-- | A useful pattern synonym for using 'Append' with @++@ from
+-- "Data.Singletons.Prelude.List".
+--
+-- As a /pattern/, this brings @(as ++ bs) ~ cs@ into the context whenever
+-- you use it to match on an @'Append' as bs cs@.
+--
+-- As an /expression/, this constructs an @'Append' as bs cs@ as long as
+-- you have @(as ++ bs) ~ cs@ in the context.
+--
+-- @since 0.1.2.0
+pattern AppendWit :: forall as bs cs. (RecApplicative as, RecApplicative bs) => (as ++ bs) ~ cs => Append as bs cs
+pattern AppendWit <- (appendWit @as @bs @cs -> Refl)
+  where
+    AppendWit = unAppendWit @as @bs @cs pureShape pureShape
+{-# COMPLETE AppendWit #-}
+
+-- | 'appendWit' stated as a 'Predicate' implication.
+--
+-- @since 0.1.2.0
+implyAppend :: IsAppend as bs --> EqualTo (as ++ bs)
+implyAppend _ = appendWit
+
+-- | Witness that @'Append' as bs cs@ implies @(as ++ bs) ~ cs@, using
+-- @++@ from "Data.Vinyl.TypeLevel".
+--
+-- @since 0.1.2.0
+appendWitV :: Append as bs cs -> (as V.++ bs) :~: cs
+appendWitV = \case
+    AppZ -> Refl
+    AppS a -> case appendWitV a of
+      Refl -> Refl
+
+-- | The inverse of 'appendWitV': if we know @(as ++ bs) ~ cs@ (using @++@
+-- from "Data.Vinyl.TypeLevel"), we can create an @'Append' as bs cs@ given
+-- structure witnesses 'Sing'.
+--
+-- @since 0.1.2.0
+unAppendWitV
+    :: (as V.++ bs) ~ cs
+    => Rec f as
+    -> Rec f bs
+    -> Append as bs cs
+unAppendWitV = \case
+    RNil     -> \_   -> AppZ
+    _ :& xs -> AppS . unAppendWitV xs
+
+-- | A useful pattern synonym for using 'Append' with @++@ from
+-- "Data.Vinyl.TypeLevel".
+--
+-- As a /pattern/, this brings @(as ++ bs) ~ cs@ into the context whenever
+-- you use it to match on an @'Append' as bs cs@.
+--
+-- As an /expression/, this constructs an @'Append' as bs cs@ as long as
+-- you have @(as ++ bs) ~ cs@ in the context.
+--
+-- @since 0.1.2.0
+pattern AppendWitV :: forall as bs cs. (RecApplicative as, RecApplicative bs) => (as V.++ bs) ~ cs => Append as bs cs
+pattern AppendWitV <- (appendWitV @as @bs @cs -> Refl)
+  where
+    AppendWitV = unAppendWitV @as @bs @cs pureShape pureShape
+{-# COMPLETE AppendWitV #-}
+
+-- | Combine the powers of 'AppendWit' and 'AppendWitV' by matching on an
+-- 'Append' to witness @(as ++ bs) ~ cs@ for /both/ @++@ from
+-- "Data.Singletons.Prelude.List" and "Data.Vinyl.TypeLevel".  This also
+-- witnesses that @(as ++ bs) ~ (as ++ bs)@ (for the two different @++@s)
+-- by transitive property.
+--
+-- @since 0.1.2.0
+pattern AppendWit' :: forall as bs cs. (RecApplicative as, RecApplicative bs) => ((as ++ bs) ~ cs, (as V.++ bs) ~ cs) => Append as bs cs
+pattern AppendWit' <- ((\a -> (a,a)) -> (AppendWit, AppendWitV))
+  where
+    AppendWit' = AppendWit
+{-# COMPLETE AppendWitV #-}
+
+-- | 'appendWitV' stated as a 'Predicate' implication.
+--
+-- @since 0.1.2.0
+implyAppendV :: IsAppend as bs --> EqualTo (as V.++ bs)
+implyAppendV _ = appendWitV
+
+-- | Given a witness @'Append' as bs cs@, prove that singleton's @++@ from
+-- "Data.Singletons.Prelude.List" is the same as vinyl's @++@
+-- "Data.Vinyl.TypeLevel".
+convertAppends :: Append as bs cs -> (as ++ bs) :~: (as V.++ bs)
+convertAppends a = case appendWit a of
+    Refl -> case appendWitV a of
+      Refl -> Refl
+
+-- | Given @as@ and @bs@, create an @'Append' as bs cs@ with, with @cs@
+-- existentially quantified
+withAppend :: Rec f as -> Rec f bs -> (forall cs. Rec f cs -> Append as bs cs -> r) -> r
+withAppend = \case
+    RNil -> \ys f -> f ys AppZ
+    x :& xs -> \ys f -> withAppend xs ys $ \zs a ->
+      f (x :& zs) (AppS a)
+
 -- | Witness an isomorphism between 'Rec' and two parts that compose it.
 --
 -- Read this type signature as:
@@ -278,7 +541,7 @@
 -- @bs. It is constructed by selectively zipping items from @as@ and @bs@
 -- together, like mergesort or riffle shuffle.
 --
--- You construct a 'Interleave' from @as@ and @bs@ by picking "which item" from
+-- You construct an 'Interleave' from @as@ and @bs@ by picking "which item" from
 -- @as@ and @bs@ to add to @cs@.
 --
 -- Some examples:
@@ -298,6 +561,77 @@
 
 deriving instance Show (Interleave as bs cs)
 
+-- | A type-level predicate that a given list is the "interleave" of @as@
+-- and @bs@.
+--
+-- @since 0.1.2.0
+type IsInterleave as bs = TyPred (Interleave as bs)
+
+instance Auto (IsInterleave '[] '[]) '[] where
+    auto = IntZ
+
+instance Auto (IsInterleave as bs) cs => Auto (IsInterleave (a ': as) bs) (a ': cs) where
+    auto = IntL (auto @_ @(IsInterleave as bs) @cs)
+
+instance Auto (IsInterleave as bs) cs => Auto (IsInterleave as (b ': bs)) (b ': cs) where
+    auto = IntR (auto @_ @(IsInterleave as bs) @cs)
+
+instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInterleave as bs) where
+    decide = case sing @as of
+      SNil -> case sing @bs of
+        SNil -> \case
+          SNil -> Proved IntZ
+          _ `SCons` _ -> Disproved $ \case {}
+        y `SCons` (Sing :: Sing bs') -> \case
+          z `SCons` (zs :: Sing cs') -> case y %~ z of
+            Proved Refl -> case decide @(IsInterleave '[] bs') zs of
+              Proved i -> Proved $ IntR i
+              Disproved v -> Disproved $ \case
+                IntR i -> v i
+            Disproved v -> Disproved $ \case
+              IntR _ -> v Refl
+          SNil -> Disproved $ \case {}
+      x `SCons` (Sing :: Sing as') -> case sing @bs of
+        SNil -> \case
+          z `SCons` (zs :: Sing cs') -> case x %~ z of
+            Proved Refl -> case decide @(IsInterleave as' '[]) zs of
+              Proved i -> Proved $ IntL i
+              Disproved v -> Disproved $ \case
+                IntL i -> v i
+            Disproved v -> Disproved $ \case
+              IntL _ -> v Refl
+          SNil -> Disproved $ \case {}
+        y `SCons` (Sing :: Sing bs') -> \case
+          SNil -> Disproved $ \case {}
+          z `SCons` (zs :: Sing cs') -> case x %~ z of
+            Proved Refl -> case decide @(IsInterleave as' bs) zs of
+              Proved i    -> Proved $ IntL i
+              Disproved v -> case y %~ z of
+                Proved Refl -> case decide @(IsInterleave as bs') zs of
+                  Proved i -> Proved $ IntR i
+                  Disproved u -> Disproved $ \case
+                    IntL i -> v i
+                    IntR i -> u i
+                Disproved u -> Disproved $ \case
+                  IntL i -> v i
+                  IntR _ -> u Refl
+            Disproved v -> case y %~ z of
+              Proved Refl -> case decide @(IsInterleave as bs') zs of
+                Proved i -> Proved $ IntR i
+                Disproved u -> Disproved $ \case
+                  IntL _ -> v Refl
+                  IntR i -> u i
+              Disproved u -> Disproved $ \case
+                IntL _ -> v Refl
+                IntR _ -> u Refl
+
+-- | Automatically generate an 'Interleave' if @as@ and @bs@ are known
+-- statically.
+--
+-- @since 0.1.2.0
+autoInterleave :: forall as bs cs. Auto (IsInterleave as bs) cs => Interleave as bs cs
+autoInterleave = auto @_ @(IsInterleave as bs) @cs
+
 -- | Given two 'Rec's, interleave the two to create a combined 'Rec'.
 --
 -- @since 0.1.1.0
@@ -323,6 +657,19 @@
       x :& xs -> first  (x :&) . unweaveRec m $ xs
     IntR m -> \case
       x :& xs -> second (x :&) . unweaveRec m $ xs
+
+-- | Turn an 'Interleave' into a 'Rec' of indices from either sublist.
+--
+-- Warning: O(n^2)
+--
+-- @since 0.1.2.0
+interleavedIxes :: Interleave as bs cs -> Rec (Index as :+: Index bs) cs
+interleavedIxes = \case
+    IntZ   -> RNil
+    IntL i -> L1 IZ :& VR.rmap (\case L1 i' -> L1 (IS i'); R1 j -> R1 j)
+                               (interleavedIxes i)
+    IntR j -> R1 IZ :& VR.rmap (\case L1 i -> L1 i; R1 j' -> R1 (IS j'))
+                               (interleavedIxes j)
 
 -- | Interleave an 'Index' on @as@ into a full index on @cs@, which is @as@
 -- interleaved with @bs@.