diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,4 +1,2 @@
 # gdp: Ghosts of Departed Proofs
 
-
-
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,12 +1,13 @@
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE GADTs         #-}
+{-# LANGUAGE GADTs           #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE TypeOperators   #-}
 
 module Main where
 
-import GDP
+import           GDP
 
-import Data.Ord
 import qualified Data.List as L
+import           Data.Ord
 
 -- An unsafe merge. This relies on the user remembering to
 -- sort both of the inputs using the same comparator passed
@@ -25,6 +26,7 @@
 -- Introduce a predicate `SortedBy comp`, indicating that
 -- the value has been sorted by the comparator named `comp`.
 newtype SortedBy comp name = SortedBy Defn
+type role SortedBy nominal nominal
 
 -- Sort a value using the comparator named `comp`. The
 -- resulting value will satisfy `SortedBy comp`.
@@ -43,6 +45,7 @@
 mergeBy (The comp) (The xs) (The ys) = assert (unsafeMergeBy comp xs ys)
 
 newtype Opposite comp = Opposite Defn
+type role Opposite nominal
 
 -- A named version of the opposite ordering.
 opposite :: ((a -> a -> Ordering) ~~ comp)
@@ -53,6 +56,7 @@
   LT -> GT
 
 newtype Reverse xs = Reverse Defn
+type role Reverse nominal
 
 -- A named version of Prelude's 'reverse'.
 rev :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)
diff --git a/gdp.cabal b/gdp.cabal
--- a/gdp.cabal
+++ b/gdp.cabal
@@ -1,5 +1,5 @@
 name:                gdp
-version:             0.0.0.2
+version:             0.0.3.0
 synopsis:            Reason about invariants and preconditions with ghosts of departed proofs.
 description:         Reason about invariants and preconditions with ghosts of departed proofs.
                      The GDP library implements building blocks for creating and working with
@@ -8,7 +8,7 @@
                      so that they will be statically checked at compile-time.
                      As a library user, you can use the `gdp` deduction rules to codify your
                      proofs that you are using the library correctly.
-homepage:            https://github.com/githubuser/gdp#readme
+homepage:            https://github.com/matt-noonan/gdp#readme
 license:             BSD3
 license-file:        LICENSE
 author:              Matt Noonan
@@ -26,11 +26,13 @@
                      , Data.Refined
                      , Data.The
                      , Logic.Classes
+                     , Logic.Implicit
                      , Logic.NegClasses
                      , Logic.Propositional
                      , Logic.Proof
                      , Theory.Equality
                      , Theory.Named
+                     , Theory.Lists
                      
   build-depends:       base >= 4.7 && < 5
                      , lawful
diff --git a/src/Data/Arguments.hs b/src/Data/Arguments.hs
--- a/src/Data/Arguments.hs
+++ b/src/Data/Arguments.hs
@@ -23,7 +23,7 @@
 --   This is entirely a type-level operation, there
 --   is nothing corresponding to a value access or update.
 class Argument (f :: k1) (n :: k2) where
-  type GetArg f n   :: k1
+  type GetArg f n   :: k
   type SetArg f n x :: k1
 
 -- | Position: the left-hand side of a type.
diff --git a/src/Data/Refined.hs b/src/Data/Refined.hs
--- a/src/Data/Refined.hs
+++ b/src/Data/Refined.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE KindSignatures        #-}
 {-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE RoleAnnotations       #-}
 
 {-|
   Module      :  Data.Refined
@@ -61,6 +62,7 @@
 -}
 newtype a ::: p = SuchThat a
 infixr 1 :::
+type role (:::) nominal nominal
 
 instance The a' a => The (a' ::: p) a where
   the (SuchThat x) = the x
@@ -102,6 +104,7 @@
     run-time space or time cost.
 -}
 newtype Satisfies (p :: * -> *) a = Satisfies a
+type role Satisfies nominal nominal
 instance The (Satisfies p a) a
 
 -- | An infix alias for 'Satisfies'.
@@ -130,7 +133,10 @@
 
 @
 newtype NonEmpty xs = NonEmpty Defn
+type role Nonempty nominal -- disallows coercion of Nonempty's argument.
+
 newtype Reverse  xs = Reverse  Defn
+type role Reverse nominal
 
 rev :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)
 rev xs = defn (reverse (the xs))
diff --git a/src/GDP.hs b/src/GDP.hs
--- a/src/GDP.hs
+++ b/src/GDP.hs
@@ -11,6 +11,7 @@
   , module Data.Refined
   , module Data.The
   , module Logic.Classes
+  , module Logic.Implicit
   , module Logic.NegClasses
   , module Logic.Proof
   , module Logic.Propositional
@@ -18,12 +19,13 @@
   , module Theory.Named
   ) where
 
-import Data.Arguments
-import Data.Refined
-import Data.The
-import Logic.Classes
-import Logic.NegClasses
-import Logic.Proof
-import Logic.Propositional
-import Theory.Equality
-import Theory.Named
+import           Data.Arguments
+import           Data.Refined
+import           Data.The
+import           Logic.Classes
+import           Logic.Implicit
+import           Logic.NegClasses
+import           Logic.Proof
+import           Logic.Propositional
+import           Theory.Equality
+import           Theory.Named
diff --git a/src/Logic/Classes.hs b/src/Logic/Classes.hs
--- a/src/Logic/Classes.hs
+++ b/src/Logic/Classes.hs
@@ -1,7 +1,6 @@
 {-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE DefaultSignatures     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE PolyKinds             #-}
 
 {-|
   Module      :  Logic.Classes
@@ -30,7 +29,6 @@
 
 import Logic.Proof
 import Theory.Equality
-import Theory.Named
 
 {--------------------------------------------------------
   Special properties of predicates and functions
@@ -46,13 +44,12 @@
 
 @
 -- Define a reflexive binary relation
-newtype SameColor p q = SameColor Defn
+data SameColor p q
 instance Reflexive SameColor
 @
--}   
+-}
 class Reflexive r where
   refl :: Proof (r x x)
-  default refl :: (Defining (r x x)) => Proof (r x x)
   refl = axiom
 
 {-| A binary relation R is /symmetric/ if, for all x and y,
@@ -66,13 +63,12 @@
 
 @
 -- Define a symmetric binary relation
-newtype NextTo p q = NextTo Defn
+data NextTo p q
 instance Symmetric NextTo
 @
--}   
+-}
 class Symmetric c where
-  symmetric :: c p q -> Proof (c q p)
-  default symmetric :: (Defining (c p q)) => c p q -> Proof (c q p)
+  symmetric :: Proof (c p q) -> Proof (c q p)
   symmetric _ = axiom
 
 {-| A binary relation R is /transitive/ if, for all x, y, z,
@@ -86,17 +82,16 @@
 
 @
 -- Define a transitive binary relation
-newtype CanReach p q = CanReach Defn
+data CanReach p q
 instance Transitive CanReach
 @
--}   
+-}
 class Transitive c where
-  transitive :: c p q -> c q r -> Proof (c p r)
-  default transitive :: Defining (c p q) => c p q -> c q r -> Proof (c p r)
+  transitive :: Proof (c p q) -> Proof (c q r) -> Proof (c p r)
   transitive _ _ = axiom
 
 -- | @transitive@, with the arguments flipped.
-transitive' :: Transitive c => c q r -> c p q -> Proof (c p r)
+transitive' :: Transitive c => Proof (c q r) -> Proof (c p q) -> Proof (c p r)
 transitive' = flip transitive
 
 {-| A binary operation @#@ is idempotent if @x # x == x@ for all @x@.
@@ -108,15 +103,14 @@
 
 @
 -- Define an idempotent binary operation
-newtype Union x y = Union Defn
+data Union x y
 instance Idempotent Union
 @
 -}
 class Idempotent c where
   idempotent :: Proof (c p p == p)
-  default idempotent :: Defining (c p p) => Proof (c p p == p)
   idempotent = axiom
-  
+
 {-| A binary operation @#@ is commutative if @x # y == y # x@ for all @x@ and @y@.
     The @Commutative c@ typeclass provides a single method,
     @commutative :: Proof (c x y == c y x)@.
@@ -126,13 +120,12 @@
 
 @
 -- Define a commutative binary operation
-newtype Union x y = Union Defn
+data Union x y
 instance Commutative Union
 @
 -}
 class Commutative c where
   commutative :: Proof (c p q == c q p)
-  default commutative :: Defining (c p q) => Proof (c p q == c q p)
   commutative = axiom
 
 {-| A binary operation @#@ is associative if @x # (y # z) == (x # y) # z@ for
@@ -145,13 +138,12 @@
 
 @
 -- Define an associative binary operation
-newtype Union x y = Union Defn
+data Union x y
 instance Associative Union
 @
 -}
 class Associative c where
   associative :: Proof (c p (c q r) == c (c p q) r)
-  default associative :: Defining (c p q) => Proof (c p (c q r) == c (c p q) r)
   associative = axiom
 
 {-| A binary operation @#@ distributes over @%@ on the left if
@@ -165,14 +157,13 @@
 
 @
 -- x `Union` (y `Intersect` z) == (x `Union` y) `Intersect` (x `Union` z)
-newtype Union     x y = Union     Defn
-newtype Intersect x y = Intersect Defn
+data Union     x y
+data Intersect x y
 instance DistributiveL Union Intersect
 @
 -}
 class DistributiveL c c' where
   distributiveL :: Proof (c p (c' q r) == c' (c p q) (c p r))
-  default distributiveL :: (Defining (c p q), Defining (c' p q)) => Proof (c p (c' q r) == c' (c p q) (c p r))
   distributiveL = axiom
 
 {-| A binary operation @#@ distributes over @%@ on the right if
@@ -186,14 +177,13 @@
 
 @
 -- (x `Intersect` y) `Union` z == (x `Union` z) `Intersect` (y `Union` z)
-newtype Union     x y = Union     Defn
-newtype Intersect x y = Intersect Defn
+data Union     x y
+data Intersect x y
 instance DistributiveR Union Intersect
 @
 -}
 class DistributiveR c c' where
   distributiveR :: Proof (c (c' p q) r == c' (c p r) (c q r))
-  default distributiveR :: (Defining (c p q), Defining (c' p q)) => Proof (c (c' p q) r == c' (c p r) (c q r))
   distributiveR = axiom
 
 {-| A function @f@ is /injective/ if @f x == f y@ implies @x == y@.
@@ -205,13 +195,12 @@
 
 @
 -- {x} == {y} implies x == y.
-newtype Singleton x = Singleton Defn
+data Singleton x
 instance Injective Singleton
 @
 -}
 class Injective f where
-  elim_inj :: (f x == f y) -> Proof (x == y)
-  default elim_inj :: (Defining (f x), Defining (f y)) => (f x == f y) -> Proof (x == y)
+  elim_inj :: Proof (f x == f y) -> Proof (x == y)
   elim_inj _ = axiom
 
 
diff --git a/src/Logic/Implicit.hs b/src/Logic/Implicit.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Implicit.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE RoleAnnotations     #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
+
+module Logic.Implicit
+    ( Fact
+    , known
+    , note
+    , on
+    ) where
+
+import           Logic.Proof
+import           Theory.Named
+
+import           Unsafe.Coerce
+
+-- | A @Fact p@ is an implicit proof of @p@, propagated by Haskell's constraint solver.
+--   @Fact@s can be used to implicitly introduce or propagate proofs. However, there is
+--   a small run-time cost associated with using @Fact@s: typeclass dictionaries for
+--   @Fact@s are still passed around. In many cases they will be optimized away, but this
+--   is not guaranteed.
+class Fact p
+
+-- | Recall a known @Fact@ from the implicit context.
+known :: Fact p => Proof p
+known = axiom
+
+newtype WithFact p t = WithFact (Fact p => t)
+type role WithFact nominal nominal
+
+-- | Add a proof to the implicit context.
+note :: forall p t. Proof p -> (Fact p => t) -> t
+note _ k = unsafeCoerce (WithFact k :: WithFact p t) ()
+
+{-| Apply an implication to a predicate in the implicit context. The @(a ~~ n)@
+    parameter is not actually used; it's type is used to help select a specific
+    fact from the context.
+
+@
+-- A safe 'head' function, using an implicitly-passed safety proof.
+head :: Fact (IsCons xs) => ([a] ~~ xs) -> a
+head xs = Prelude.head (the xs)
+
+-- Reverse, and a lemma.
+reverse :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)
+revConsLemma :: Proof (IsCons xs) -> Proof (IsCons (Reverse xs))
+
+-- Implement a safe 'last' function.
+last :: Fact (IsCons xs) => ([a] ~~ xs) -> a
+last xs = note (revConsLemma `on` xs) $ head (reverse xs)
+-}
+on :: Fact (p n) => (Proof (p n) -> Proof q) -> (a ~~ n) -> Proof q
+on impl _ = impl known
diff --git a/src/Logic/NegClasses.hs b/src/Logic/NegClasses.hs
--- a/src/Logic/NegClasses.hs
+++ b/src/Logic/NegClasses.hs
@@ -1,7 +1,5 @@
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE DefaultSignatures     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE PolyKinds             #-}
 
 {-|
   Module      :  Logic.NegClasses
@@ -17,10 +15,8 @@
   , Antisymmetric(..)
   ) where
 
-import Logic.Proof
-import Logic.Propositional (Not)
-import Theory.Equality
-import Theory.Named
+import           Logic.Proof
+import           Logic.Propositional (Not)
 
 {--------------------------------------------------------
   Special properties of predicates and functions
@@ -37,12 +33,12 @@
 @
 -- Define an irreflexive binary relation
 newtype DifferentColor p q = DifferentColor Defn
+type role DifferentColor nominal nominal
 instance Irreflexive DifferentColor
 @
 -}
 class Irreflexive r where
   irrefl :: Proof (Not (r x x))
-  default irrefl :: (Defining (r x x)) => Proof (Not (r x x))
   irrefl = axiom
 
 
@@ -58,10 +54,10 @@
 @
 -- Define an antisymmetric binary relation
 newtype AncestorOf p q = AncestorOf Defn
+type role DifferentColor nominal nominal
 instance Antisymmetric AncestorOf
 @
--}   
+-}
 class Antisymmetric c where
-  antisymmetric :: c p q -> Proof (Not (c q p))
-  default antisymmetric :: Defining (c p q) => c p q -> Proof (Not (c q p))
+  antisymmetric :: Proof (c p q) -> Proof (Not (c q p))
   antisymmetric _ = axiom
diff --git a/src/Logic/Proof.hs b/src/Logic/Proof.hs
--- a/src/Logic/Proof.hs
+++ b/src/Logic/Proof.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds      #-}
 
 {-|
   Module      :  Logic.Proof
@@ -9,43 +10,35 @@
 -}
 
 module Logic.Proof
-  ( -- * The `Proof` monad
+  ( -- * The `Proof` type
     Proof
-  , (|.), (|$), (|/), (|\), ($$)
-  , given
   , axiom, sorry
   ) where
 
-import Data.Coerce
-import Control.Monad ((>=>))
-
 {--------------------------------------------------
-  The `Proof` monad
+  The `Proof` type
 --------------------------------------------------}
 
-{-| The @Proof@ monad is used as a domain-specific
+{-| The @Proof@ type is used as a domain-specific
     language for constructing proofs. A value of type
     @Proof p@ represents a proof of the proposition @p@.
 
-    For example, this function constructions a proof of
-    "P or Q" from the assumption "P and Q":
+    A @Proof@ as an argument to a function represents an
+    assumption. For example, this function constructions a proof of "P
+    or Q" from the assumption "P and Q":
 
-> and2or :: (p && q) -> Proof (p || q)
+> and2or :: Proof (p && q) -> Proof (p || q)
 >
-> and2or pq = do
->    p <- and_elimL pq    -- or: "p <- fst <$> and_elim pq"
->    or_introL p
+> and2or pq = introOrL $ elimAndL pq
 
     If the body of the proof does not match the proposition
     you claim to be proving, the compiler will raise a type
     error. Here, we accidentally try to use @or_introR@
     instead of @or_introL@:
 
-> and2or :: (p && q) -> Proof (p || q)
+> and2or :: Proof (p && q) -> Proof (p || q)
 >
-> and2or pq = do
->    p <- and_elimL pq
->    or_introR p
+> and2or pq = introOrR $ elimAndL pq
 
 resulting in the error
 
@@ -53,126 +46,17 @@
     • Couldn't match type ‘p’ with ‘q’
       ‘p’ is a rigid type variable bound by
         the type signature for:
-          and2or :: forall p q. (p && q) -> Proof (p || q)
+          and2or :: forall p q. Proof (p && q) -> Proof (p || q)
 
       ‘q’ is a rigid type variable bound by
         the type signature for:
-          and2or :: forall p q. (p && q) -> Proof (p || q)
+          and2or :: forall p q. Proof (p && q) -> Proof (p || q)
 
       Expected type: Proof (p || q)
         Actual type: Proof (p || p)
 @
 -}
-data Proof (pf :: *) = QED
-
-instance Functor Proof where
-  fmap _ = const QED -- modus ponens (external?)
-
-instance Applicative Proof where
-  pure = const QED -- axiom
-  pf1 <*> pf2 = QED -- modus ponens (internal?)
-
-instance Monad Proof where
-  pf >>= f = QED
-
-{-| This operator is just a specialization of @(>>=)@, but
-    can be used to create nicely delineated chains of
-    derivations within a larger proof. The first statement
-    in the chain should produce a formula; @(|$)@ then
-    pipes this formula into the following derivation rule.
-
-> and2or :: (p && q) -> Proof (p || q)
->
-> and2or pq =  and_elimL pq
->           |$ or_introL
--}
-
-(|$) :: Proof p -> (p -> Proof q) -> Proof q
-(|$) = (>>=)
-
-infixr 7 |$
-
---(|-) :: ((p -> Proof r) -> Proof r) -> (p -> Proof r) -> Proof r
-
-{-| This operator is used to create nicely delineated chains of
-    derivations within a larger proof. If X and Y are two
-    deduction rules, each with a single premise and a single
-    conclusion, and the premise of Y matches the conclusion of X,
-    then @X |. Y@ represents the composition of the two
-    deduction rules.
-
-> and2or :: (p && q) -> Proof (p || q)
->
-> and2or =  and_elimL
->        |. or_introL
--}
-
-(|.) :: (p -> Proof q) -> (q -> Proof r) -> p -> Proof r
-(|.) = (>=>)
-
-infixr 9 |.
-
-{-| The @(|/)@ operator is used to feed the remainder of the proof in
-    as a premise of the first argument.
-
-    A common use-case is with the @Or@-elimination rules @or_elimL@ and
-    @or_elimR@, when one case is trivial. For example, suppose we wanted
-    to prove that @R && (P or (Q and (Q implies P)))@ implies @P@:
-
-@
-my_proof :: r && (p || (q && (q --> p))) -> Proof p
-
-my_proof =
-  do  and_elimR          -- Forget the irrelevant r.
-   |. or_elimL given     -- The first case of the || is immediate;
-   |/ and_elim           -- The rest of the proof handles the second case,
-   |. uncurry impl_elim  --   by unpacking the && and feeding the q into
-                         --   the implication (q --> p).
-@
-
-    The rising @/@ is meant to suggest the bottom half of the proof getting
-    plugged in to the Or-elimination line.
--}
-(|/) :: (p -> (q -> Proof r) -> Proof r) -> (q -> Proof r) -> p -> Proof r
-(|/) = flip
-infixr 9 |/
-
-{-| The @(|\\)@ operator is used to take the subproof so far and feed it
-    into a rule that is expecting a subproof as a premise.
-
-    A common use-case is with the @Not@-introduction rule @not_intro@,
-    which has a type that fits the second argument of @(|\\)@. By way
-    of example, here is a proof that "P implies Q" along with "Not Q"
-    implies "Not P".
-
-@
-my_proof :: (p --> q) -> (Not p --> r) -> Not q -> Proof r
-
-my_proof impl1 impl2 q' =
-  do  modus_ponens impl1   -- This line, composed with the next,
-   |. contradicts' q'      --   form a proof of FALSE from p.
-   |\\ not_intro            -- Closing the subproof above, conclude not-p.
-   |. modus_ponens impl2   -- Now apply the second implication to conclude r.
-@
-
-    The falling @\\@ is meant to suggest the upper half of the proof
-    being closed off by the Not-introduction line.
--}
-(|\) :: (p -> Proof q) -> ((p -> Proof q) -> Proof r) -> Proof r
-(|\) = flip ($)
-infixl 8 |\
-
--- | Take a proof of @p@ and feed it in as the first premise of
---   an argument that expects a @p@ and a @q@.
-($$) :: (p -> q -> Proof r) -> Proof p -> (q -> Proof r)
-(f $$ pp) q = do { p <- pp; f p q }
-
--- | @given@ creates a proof of P, given P as
---   an assumption.
---
---   @given@ is just a specialization of @pure@ / @return@.
-given :: p -> Proof p
-given _ = QED
+data Proof (pf :: k) = QED
 
 -- | @sorry@ can be used to provide a "proof" of
 --   any proposition, by simply assering it as
@@ -183,6 +67,7 @@
 -- _Completed proofs should never use @sorry@!_
 sorry :: Proof p
 sorry = QED
+{-# WARNING sorry "Completed proofs should never use sorry!" #-}
 
 {-| @axiom@, like @sorry@, provides a "proof" of any
     proposition. Unlike @sorry@, which is used to indicate
@@ -194,10 +79,9 @@
 data Reverse xs = Reverse Defn
 data Length  xs = Length  Defn
 
-rev_length_lemma :: Proof (Length (Reverse xs) == Length xs)
-rev_length_lemma = axiom
+revLengthLemma :: Proof (Length (Reverse xs) == Length xs)
+revLengthLemma = axiom
 @
 -}
 axiom :: Proof p
 axiom = QED
-
diff --git a/src/Logic/Propositional.hs b/src/Logic/Propositional.hs
--- a/src/Logic/Propositional.hs
+++ b/src/Logic/Propositional.hs
@@ -1,15 +1,8 @@
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE RankNTypes            #-}
-{-# LANGUAGE KindSignatures        #-}
-{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE ExplicitNamespaces    #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE DefaultSignatures     #-}
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE UndecidableSuperClasses #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE PolyKinds             #-}
 
 {-|
   Module      :  Logic.Propositional
@@ -24,7 +17,7 @@
 
   -- ** Logical symbols
     TRUE, FALSE
-  
+
   , And,     type (&&), type (∧), type (/\)
   , Or,      type (||), type (∨), type (\/)
   , Implies, type (-->)
@@ -42,92 +35,97 @@
 
   -- | Introduction rules give the elementary building blocks
   --   for creating a formula from simpler ones.
-  , and_intro
-  , or_introL
-  , or_introR
-  , impl_intro
-  , not_intro
+  , introAnd
+  , introAnd'
+
+  , introOrL
+  , introOrR
+
+  , introImpl
+  , introNot
+
   , contrapositive
   , contradicts
   , contradicts'
-  , univ_intro
-  , ex_intro
+  , introUniv
+  , introEx
 
   -- *** Elimination rules
 
   -- | Elimination rules give the elementary building blocks for
   --   decomposing a complex formula into simpler ones.
-  , and_elimL
-  , and_elimR
-  , and_elim
-  , or_elim
-  , or_elimL
-  , or_elimR
-  , impl_elim
-  , modus_ponens
-  , modus_tollens
+  , elimAndL
+  , elimAndR
+
+  , elimOr
+  , elimOrL
+  , elimOrR
+
+  , elimImpl
+  , modusPonens
+  , modusTollens
   , absurd
-  , univ_elim
-  , ex_elim
+  , elimUniv
+  , elimEx
 
   -- *** Classical logic and the Law of the Excluded Middle
   , Classical
   , classically
   , lem
   , contradiction
-  , not_not_elim
+  , elimNot
+  , elimNotNot
 
-   -- *** Mapping over conjunctions and disjunctions
-  , and_mapL
-  , and_mapR
-  , and_map
+  -- *** Mapping over conjunctions and disjunctions.
 
-  , or_mapL
-  , or_mapR
-  , or_map
+  -- | These function names mimic the ones for
+  -- (@Functor@/@Bifunctor@/@Profunctor@).
+  , firstAnd
+  , secondAnd
+  , bimapAnd
 
-  , impl_mapL
-  , impl_mapR
-  , impl_map
+  , firstOr
+  , secondOr
+  , bimapOr
 
-  , not_map
+  , lmapImpl
+  , rmapImpl
+  , dimapImpl
 
+  , mapNot
+
   ) where
 
-import Data.Arguments
-import Data.Refined
-import Data.The
 import Logic.Classes
 import Logic.Proof
-import Theory.Named
 
 {--------------------------------------------------
   Logical constants
 --------------------------------------------------}
 
 -- | The constant "true".
-newtype TRUE  = TRUE Defn
+data TRUE
 
 -- | The constant "false".
-newtype FALSE = FALSE Defn
+data FALSE
 
 -- | The conjunction of @p@ and @q@.
-newtype And p q = And Defn
+data And p q
 
 -- | The disjunction of @p@ and @q@.
-newtype Or p q  = Or  Defn
+data Or p q
 
 -- | The negation of @p@.
-newtype Not p   = Not Defn
+data Not p
 
 -- | The implication "@p@ implies @q@".
-newtype Implies p q = Implies Defn
+data Implies p q
 
 -- | Existential quantifiation.
-newtype Exists x p = Exists Defn
+data Exists x p
 
 -- | Universal quantification.
-newtype ForAll x p = ForAll Defn
+data ForAll x p
 
 -- | An infix alias for @Or@.
 type p || q   = p `Or` q
@@ -168,54 +166,48 @@
 --------------------------------------------------}
 
 -- | Apply a derivation to the left side of a conjunction.
-and_mapL :: (p -> Proof p') -> (p && q) -> Proof (p' && q)
-and_mapL impl conj = do
-  (lhs, rhs) <- and_elim conj
-  lhs' <- impl lhs
-  and_intro lhs' rhs
+firstAnd :: (Proof p -> Proof p') -> Proof (p && q) -> Proof (p' && q)
+firstAnd = flip bimapAnd id
 
 -- | Apply a derivation to the right side of a conjunction.
-and_mapR :: (q -> Proof q') -> (p && q) -> Proof (p && q')
-and_mapR impl conj = do
-  (lhs, rhs) <- and_elim conj
-  rhs' <- impl rhs
-  and_intro lhs rhs'
+secondAnd :: (Proof q -> Proof q') -> Proof (p && q) -> Proof (p && q')
+secondAnd = bimapAnd id
 
 -- | Apply derivations to the left and right sides of a conjunction.
-and_map :: (p -> Proof p') -> (q -> Proof q') -> (p && q) -> Proof (p' && q')
-and_map implP implQ conj = do
-  (lhs, rhs) <- and_elim conj
-  lhs' <- implP lhs
-  rhs' <- implQ rhs
-  and_intro lhs' rhs'
+bimapAnd :: (Proof p -> Proof p') -> (Proof q -> Proof q') -> Proof (p && q) -> Proof (p' && q')
+bimapAnd implP implQ conj = let
+  (lhs, rhs) = elimAnd conj
+  lhs' = implP lhs
+  rhs' = implQ rhs
+  in introAnd lhs' rhs'
 
 -- | Apply a derivation to the left side of a disjunction.
-or_mapL :: (p -> Proof p') -> (p || q) -> Proof (p' || q)
-or_mapL impl = or_elim (impl |. or_introL) or_introR
+firstOr :: (Proof p -> Proof p') -> Proof (p || q) -> Proof (p' || q)
+firstOr = flip bimapOr id
 
 -- | Apply a derivation to the right side of a disjunction.
-or_mapR :: (q -> Proof q') -> (p || q) -> Proof (p || q')
-or_mapR impl = or_elim or_introL (impl |. or_introR)
+secondOr :: (Proof q -> Proof q') -> Proof (p || q) -> Proof (p || q')
+secondOr = bimapOr id
 
 -- | Apply derivations to the left and right sides of a disjunction.
-or_map :: (p -> Proof p') -> (q -> Proof q') -> (p || q) -> Proof (p' || q')
-or_map implP implQ = or_elim (implP |. or_introL) (implQ |. or_introR)
+bimapOr :: (Proof p -> Proof p') -> (Proof q -> Proof q') -> Proof (p || q) -> Proof (p' || q')
+bimapOr implP implQ = elimOr (introOrL . implP) (introOrR . implQ)
 
 -- | Apply a derivation to the left side of an implication.
-impl_mapL :: (p' -> Proof p) -> (p --> q) -> Proof (p' --> q)
-impl_mapL derv impl = impl_intro (derv |. modus_ponens impl)
+lmapImpl :: (Proof p' -> Proof p) -> Proof (p --> q) -> Proof (p' --> q)
+lmapImpl = flip dimapImpl id
 
 -- | Apply a derivation to the right side of an implication.
-impl_mapR :: (q -> Proof q') -> (p --> q) -> Proof (p --> q')
-impl_mapR derv impl = impl_intro (modus_ponens impl |. derv)
+rmapImpl :: (Proof q -> Proof q') -> Proof (p --> q) -> Proof (p --> q')
+rmapImpl = dimapImpl id
 
 -- | Apply derivations to the left and right sides of an implication.
-impl_map :: (p' -> Proof p) -> (q -> Proof q') -> (p --> q) -> Proof (p' --> q')
-impl_map dervL dervR impl = impl_intro (dervL |. modus_ponens impl |. dervR)
+dimapImpl :: (Proof p' -> Proof p) -> (Proof q -> Proof q') -> Proof (p --> q) -> Proof (p' --> q')
+dimapImpl dervL dervR impl = introImpl (dervR . modusPonens impl . dervL)
 
 -- | Apply a derivation inside of a negation.
-not_map :: (p' -> Proof p) -> Not p -> Proof (Not p')
-not_map impl notP = not_intro (impl |. contradicts' notP |. absurd)
+mapNot :: (Proof p' -> Proof p) -> Proof (Not p) -> Proof (Not p')
+mapNot impl notP = introNot (absurd . contradicts' notP . impl)
 
 {--------------------------------------------------
   Tautologies
@@ -234,100 +226,97 @@
 --------------------------------------------------}
 
 -- | Prove "P and Q" from P and Q.
-and_intro :: p -> q -> Proof (p && q)
-and_intro _ _ = axiom
+introAnd :: Proof p -> Proof q -> Proof (p && q)
+introAnd _ _ = axiom
 
 -- | Prove "P and Q" from Q and P.
-and_intro' :: q -> p -> Proof (p && q)
-and_intro' _ _ = axiom
+introAnd' :: Proof q -> Proof p -> Proof (p && q)
+introAnd' _ _ = axiom
 
 -- | Prove "P or Q" from  P.
-or_introL :: p -> Proof (p || q)
-or_introL _ = axiom
+introOrL :: Proof p -> Proof (p || q)
+introOrL _ = axiom
 
 -- | Prove "P or Q" from Q.
-or_introR :: q -> Proof (p || q)
-or_introR _ = axiom
+introOrR :: Proof q -> Proof (p || q)
+introOrR _ = axiom
 
 -- | Prove "P implies Q" by demonstrating that,
 --   from the assumption P, you can prove Q.
-impl_intro :: (p -> Proof q) -> Proof (p --> q)
-impl_intro _ = axiom
+introImpl :: (Proof p -> Proof q) -> Proof (p --> q)
+introImpl _ = axiom
 
 -- | Prove "not P" by demonstrating that,
 --   from the assumption P, you can derive a false conclusion.
-not_intro :: (p -> Proof FALSE) -> Proof (Not p)
-not_intro _ = axiom
+introNot :: (Proof p -> Proof FALSE) -> Proof (Not p)
+introNot _ = axiom
 
--- | `contrapositive` is an alias for `not_intro`, with
+-- | `contrapositive` is an alias for `introNot`, with
 --   a somewhat more suggestive name. Not-introduction
 --   corresponds to the proof technique "proof by contrapositive".
-contrapositive :: (p -> Proof FALSE) -> Proof (Not p)
-contrapositive = not_intro
+contrapositive :: (Proof p -> Proof FALSE) -> Proof (Not p)
+contrapositive = introNot
 
 -- | Prove a contradiction from "P" and "not P".
-contradicts :: p -> Not p -> Proof FALSE
+contradicts :: Proof p -> Proof (Not p) -> Proof FALSE
 contradicts _ _ = axiom
 
 -- | `contradicts'` is `contradicts` with the arguments
 --   flipped. It is useful when you want to partially
 --   apply `contradicts` to a negation.
-contradicts' :: Not p -> p -> Proof FALSE
+contradicts' :: Proof (Not p) -> Proof p -> Proof FALSE
 contradicts' = flip contradicts
 
 -- | Prove "For all x, P(x)" from a proof of P(*c*) with
 --   *c* indeterminate.
-univ_intro :: (forall c. Proof (p c)) -> Proof (ForAll x (p x))
-univ_intro _ = axiom
+introUniv :: (forall c. Proof (p c)) -> Proof (ForAll x (p x))
+introUniv _ = axiom
 
 -- | Prove "There exists an x such that P(x)" from a specific
 --   instance of P(c).
-ex_intro :: p c -> Proof (Exists x (p x))
-ex_intro _ = axiom
+introEx :: Proof (p c) -> Proof (Exists x (p x))
+introEx _ = axiom
 
 {--------------------------------------------------
   Elimination rules
 --------------------------------------------------}
 
 -- | From the assumption "P and Q", produce a proof of P.
-and_elimL :: p && q -> Proof p
-and_elimL _ = axiom
+elimAndL :: Proof (p && q) -> Proof p
+elimAndL _ = axiom
 
 -- | From the assumption "P and Q", produce a proof of Q.
-and_elimR :: p && q -> Proof q
-and_elimR _ = axiom
+elimAndR :: Proof (p && q) -> Proof q
+elimAndR _ = axiom
 
 -- | From the assumption "P and Q", produce both a proof
 --   of P, and a proof of Q.
-and_elim :: p && q -> Proof (p, q)
-and_elim c = (,) <$> and_elimL c <*> and_elimR c
-  
-{-| If you have a proof of R from P, and a proof of
-     R from Q, then convert "P or Q" into a proof of R.
--}
-or_elim :: (p -> Proof r) -> (q -> Proof r) -> (p || q) -> Proof r
-or_elim _ _ _ = axiom
+elimAnd :: Proof (p && q) -> (Proof p, Proof q)
+elimAnd c = (elimAndL c, elimAndR c)
 
-{-| Eliminate the first alternative in a conjunction.
--}
-or_elimL :: (p -> Proof r) -> (p || q) -> (q -> Proof r) -> Proof r
-or_elimL case1 disj case2 = or_elim case1 case2 disj
+-- | If you have a proof of R from P, and a proof of R from Q, then
+--   convert "P or Q" into a proof of R.
+elimOr :: (Proof p -> Proof r) -> (Proof q -> Proof r) -> Proof (p || q) -> Proof r
+elimOr _ _ _ = axiom
 
-{-| Eliminate the second alternative in a conjunction.
--}
-or_elimR :: (q -> Proof r) -> (p || q) -> (p -> Proof r) -> Proof r
-or_elimR case2 disj case1 = or_elim case1 case2 disj
+-- | Eliminate the first alternative in a conjunction.
+elimOrL :: (Proof p -> Proof r) -> Proof (p || q) -> (Proof q -> Proof r) -> Proof r
+elimOrL case1 disj case2 = elimOr case1 case2 disj
 
+-- | Eliminate the second alternative in a conjunction.
+elimOrR :: (Proof q -> Proof r) -> Proof (p || q) -> (Proof p -> Proof r) -> Proof r
+elimOrR case2 disj case1 = elimOr case1 case2 disj
+
 -- | Given "P imples Q" and P, produce a proof of Q.
 --   (modus ponens)
-impl_elim :: p -> (p --> q) -> Proof q
-impl_elim _ _ = axiom
+elimImpl :: Proof p -> Proof (p --> q) -> Proof q
+elimImpl _ _ = axiom
 
--- | @modus_ponens@ is just @impl_elim@ with the arguments
+-- | @modusPonens@ is just `elimImpl` with the arguments
 --   flipped. In this form, it is useful for partially
 --   applying an implication.
-modus_ponens :: (p --> q) -> p -> Proof q
-modus_ponens = flip impl_elim
+modusPonens :: Proof (p --> q) -> Proof p -> Proof q
+modusPonens = flip elimImpl
 
 {-| Modus tollens lets you prove "Not P" from
     "P implies Q" and "Not Q".
@@ -339,46 +328,39 @@
                                   -----         (assumption)
                         p --> q,    p
                        ---------------------    (modus ponens)
-                 q,           Not q    
+               Not q,            q
               --------------------------        (contradicts')
                       FALSE
           ------------------------------------- (not-intro)
                              Not p
 @
 
-We can encode this proof tree more-or-less directly as a @Proof@
-to implement @modus_tollens@:
+We can encode this proof tree as a @Proof@ to implement
+@modus_tollens@:
 
 @
-modus_tollens :: (p --> q) -> Not q -> Proof (Not p)
-
-modus_tollens impl q' =
-  do  modus_ponens impl
-   |. contradicts' q'
-   |\\ not_intro
+modusTollens :: Proof (p --> q) -> Proof (Not q) -> Proof (Not p)
+modusTollens impl q' = introNot $ \p -> contradicts' q' (modusPonens impl p)
 @
 -}
 
-modus_tollens :: (p --> q) -> Not q -> Proof (Not p)
-modus_tollens impl q' =
-  do  modus_ponens impl
-   |. contradicts' q'
-   |\ not_intro
+modusTollens :: Proof (p --> q) -> Proof (Not q) -> Proof (Not p)
+modusTollens impl q' = introNot $ \p -> contradicts' q' (modusPonens impl p)
 
 -- | From a falsity, prove anything.
-absurd :: FALSE -> Proof p
+absurd :: Proof FALSE -> Proof p
 absurd _ = axiom
 
 -- | Given "For all x, P(x)" and any c, prove the proposition
 --   "P(c)".
-univ_elim :: ForAll x (p x) -> Proof (p c)
-univ_elim _ = axiom
+elimUniv :: Proof (ForAll x (p x)) -> Proof (p c)
+elimUniv _ = axiom
 
 -- | Given a proof of Q from P(c) with c generic, and the
 --   statement "There exists an x such that P(x)", produce
 --   a proof of Q.
-ex_elim :: (forall c. p c -> Proof q) -> Exists x (p x) -> Proof q
-ex_elim _ _ = axiom
+elimEx :: (forall c. Proof (p c) -> Proof q) -> Proof (Exists x (p x)) -> Proof q
+elimEx _ _ = axiom
 
 
 {--------------------------------------------------
@@ -409,7 +391,7 @@
 {-| Proof by contradiction: this proof technique allows
      you to prove P by showing that, from "Not P", you
      can prove a falsehood.
-  
+
      Proof by contradiction is not a theorem of
      constructive logic, so it requires the @Classical@
      constraint. But note that the similar technique
@@ -417,8 +399,8 @@
      valid in constructive logic! For comparison, the two types are:
 
 @
-contradiction  :: Classical => (Not p -> Proof FALSE) -> p
-not_intro      ::              (p     -> Proof FALSE) -> Not p
+contradiction  :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p
+introNot       ::              (Proof      p  -> Proof FALSE) -> Proof (Not p)
 @
 
 The derivation of proof by contradiction from the law of the excluded
@@ -429,32 +411,28 @@
 from which the desired conclusion is derived.
 
 @
-contradiction impl =
-  do  lem             -- introduce p || Not p
-   |$ or_elimL given  -- dispatch the first, straightforward case
-   |/ impl            -- Now we're on the second case. Apply the implication..
-   |. absurd          -- .. and, from falsity, conclude p.
+contradiction impl = elimOr id (absurd . impl) lem
 @
 -}
-contradiction :: forall p. Classical => (Not p -> Proof FALSE) -> Proof p
-contradiction impl =
-  do  lem
-   |$ or_elimL given
-   |/ impl
-   |. absurd
-  
+contradiction :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p
+contradiction impl = elimOr id (absurd . impl) lem
+
+-- | Alias for 'contradiction', to complete the patterns.
+elimNot :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p
+elimNot = contradiction
+
 {-| Double-negation elimination. This is another non-constructive
     proof technique, so it requires the @Classical@ constraint.
 
     The derivation of double-negation elimination follows from
     proof by contradiction, since "Not (Not p)" contradicts "Not p".
 @
-not_not_elim p'' = contradiction (contradicts' p'')
+elimNotNot p'' = contradiction (contradicts' p'')
 @
 -}
 
-not_not_elim :: Classical => Not (Not p) -> Proof p
-not_not_elim p'' = contradiction (contradicts' p'')
+elimNotNot :: Classical => Proof (Not (Not p)) -> Proof p
+elimNotNot p'' = contradiction (contradicts' p'')
 
 {--------------------------------------------------
   Algebraic properties
@@ -475,4 +453,3 @@
 instance DistributiveL And Or
 instance DistributiveL Or  And
 instance DistributiveL Or  Or
-
diff --git a/src/Theory/Equality.hs b/src/Theory/Equality.hs
--- a/src/Theory/Equality.hs
+++ b/src/Theory/Equality.hs
@@ -1,10 +1,12 @@
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE RoleAnnotations       #-}
 
 {-|
   Module      :  Theory.Equality
@@ -49,6 +51,7 @@
 --   Given an equality, you are then able to substitute one side of the equality
 --   for the other, anywhere you please.
 newtype Equals x y = Equals Defn
+type role Equals nominal nominal
 
 -- | An infix alias for 'Equals'.
 type x == y = x `Equals` y
@@ -76,25 +79,25 @@
 
 -- | Apply a function to both sides of an equality.
 apply :: forall f n x x'. (Argument f n, GetArg f n ~ x)
-    => Arg n -> (x == x') -> Proof (f == SetArg f n x')
+    => Arg n -> Proof (x == x') -> Proof (f == SetArg f n x')
 apply _ _ = axiom
 
--- | Given a formula and an equality over ones of its arguments,
+-- | Given a formula and an equality over one of its arguments,
 --   replace the left-hand side of the equality with the right-hand side.
 substitute :: (Argument f n, GetArg f n ~ x)
-    => Arg n -> (x == x') -> f -> Proof (SetArg f n x')
+    => Arg n -> Proof (x == x') -> f -> Proof (SetArg f n x')
 substitute _ _ _ = axiom
 
 -- | Substitute @x'@ for @x@ under the function @f@, on the left-hand side
 --   of an equality.
 substituteL :: (Argument f n, GetArg f n ~ x)
-    => Arg n -> (x == x') -> (f == g) -> Proof (SetArg f n x' == g)
+    => Arg n -> Proof (x == x') -> Proof (f == g) -> Proof (SetArg f n x' == g)
 substituteL _ _ _ = axiom
 
 -- | Substitute @x'@ for @x@ under the function @f@, on the right-hand side
 --   of an equality.
 substituteR :: (Argument f n, GetArg f n ~ x)
-    => Arg n -> (x == x') -> (g == f) -> Proof (g == SetArg f n x')
+    => Arg n -> Proof (x == x') -> Proof (g == f) -> Proof (g == SetArg f n x')
 substituteR _ _ _ = axiom
 
 {--------------------------------------------------
diff --git a/src/Theory/Lists.hs b/src/Theory/Lists.hs
new file mode 100644
--- /dev/null
+++ b/src/Theory/Lists.hs
@@ -0,0 +1,151 @@
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE PatternSynonyms     #-}
+{-# LANGUAGE RoleAnnotations     #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE ViewPatterns        #-}
+
+module Theory.Lists
+    ( -- * Basic functions on lists
+      head, tail, cons, nil
+      -- ** Names for parts of a list
+    , Head, Tail
+      -- ** Names for basic list operations
+    , Cons', Nil'
+      -- * Reasoning about lists
+      -- ** Predicates about list shapes
+    , IsList, IsCons, IsNil
+      -- ** Axioms about list shapes
+    , consIsList, nilIsList, listIsList
+    , listShapes, consIsCons, headOfCons, tailOfCons
+      -- ** Induction principle
+    , listInduction
+      -- * Pattern-matching on lists
+      -- ** Decompositions that use explicit evidence-passing
+    , classify, ListCase (..)
+      -- *** Pattern synonyms
+    , pattern IsCons, pattern IsNil
+      -- ** Decompositions that use implicit evidence-passing
+    , classify', ListCase' (..)
+      -- *** Pattern synonyms
+    , pattern Cons, pattern Nil
+    ) where
+
+import           Prelude             hiding (cons, head, reverse, tail)
+import qualified Prelude
+
+import           Data.The
+import           Logic.Implicit
+import           Logic.Proof
+import           Logic.Propositional
+import           Theory.Equality
+import           Theory.Named
+
+-- | Predicates about the possible shapes of lists.
+data IsList xs
+data IsCons xs
+data IsNil  xs
+
+-- | Names for the parts of a list.
+newtype Head xs = Head Defn
+type role Head nominal
+newtype Tail xs = Tail Defn
+type role Tail nominal
+
+-- | Possible shapes of a list, along with evidence that the list
+--   has the given shape.
+data ListCase a xs
+  = IsCons_ (Proof (IsCons xs)) (a ~~ Head xs) ([a] ~~ Tail xs)
+  | IsNil_  (Proof (IsNil  xs))
+
+-- | Classify a named list by shape, producing evidence that the
+--   list matches the corresponding case.
+classify :: ([a] ~~ xs) -> ListCase a xs
+classify xs = case the xs of
+    (h:t) -> IsCons_ axiom (defn h) (defn t)
+    []    -> IsNil_  axiom
+
+pattern IsCons :: Proof (IsCons xs) -> (a ~~ Head xs) -> ([a] ~~ Tail xs) -> ([a] ~~ xs)
+pattern IsCons proof hd tl <- (classify -> IsCons_ proof hd tl)
+
+pattern IsNil :: Proof (IsNil xs) -> ([a] ~~ xs)
+pattern IsNil proof <- (classify -> IsNil_ proof)
+
+-- | A variation on @ListCase@ that passes the shape facts implicitly. Pattern-matching on a
+--   constructor of @ListCase'@ will bring a shape proof into the implicit context.
+data ListCase' a xs where
+    Cons_ :: Fact (IsCons xs) => (a ~~ Head xs) -> ([a] ~~ Tail xs) -> ListCase' a xs
+    Nil_  :: Fact (IsNil  xs) => ListCase' a xs
+
+-- | Classify a named list by shape, producing /implicit/ evidence that the
+--   list matches the corresponding case.
+classify' :: forall a xs. ([a] ~~ xs) -> ListCase' a xs
+classify' xs = case the xs of
+    (h:t) -> note (axiom :: Proof (IsCons xs)) (Cons_ (defn h) (defn t))
+    []    -> note (axiom :: Proof (IsNil  xs))  Nil_
+
+pattern Cons :: () => Fact (IsCons xs) => (a ~~ Head xs) -> ([a] ~~ Tail xs) -> ([a] ~~ xs)
+pattern Cons hd tl <- (classify' -> Cons_ hd tl)
+
+pattern Nil :: () => Fact (IsNil xs) => ([a] ~~ xs)
+pattern Nil <- (classify' -> Nil_)
+
+-- | Extract the first element from a non-empty list.
+head :: Fact (IsCons xs) => ([a] ~~ xs) -> (a ~~ Head xs)
+head (The xs) = defn (Prelude.head xs)
+
+-- | Extract all but the first element from a non-empty list.
+tail :: Fact (IsCons xs) => ([a] ~~ xs) -> ([a] ~~ Tail xs)
+tail (The xs) = defn (Prelude.tail xs)
+
+-- | Construct a list from an element and another list.
+cons :: (a ~~ x) -> ([a] ~~ xs) -> ([a] ~~ Cons' x xs)
+cons (The x) (The xs) = defn (x:xs)
+
+-- | The empty list, named @Nil'@.
+nil :: ([a] ~~ Nil')
+nil = defn []
+
+-- | A name for referring to the result of a @cons@ operation.
+newtype Cons' x xs = Cons' Defn
+type role Cons' nominal nominal
+
+-- | A name for referring to the empty list.
+newtype Nil' = Nil' Defn
+
+-- | Axiom: The @head@ of @cons x y@ is @x@.
+headOfCons :: Proof (Head (Cons' x xs) == x)
+headOfCons = axiom
+
+-- | Axiom: The @tail@ of @cons x y@ is @y@.
+tailOfCons :: Proof (Tail (Cons' x xs) == xs)
+tailOfCons = axiom
+
+-- | Axiom: The result of @cons x y@ satisfies @IsCons@.
+consIsCons :: Proof (IsCons (Cons' x xs))
+consIsCons = axiom
+
+-- | Axiom: The empty list satisfies @IsNil@.
+nilIsNil :: Proof (IsNil Nil')
+nilIsNil = axiom
+
+-- | Axiom: a list @xs@ satisfies exactly one of @IsCons xs@ or @IsNil xs@.
+listShapes :: Proof (IsList xs) -> Proof ( (IsNil xs && Not (IsCons xs)) || (IsCons xs && Not (IsNil xs)) )
+listShapes _ = axiom
+
+-- | Induction principle: If a predicate @P@ is true for the empty list, and
+--   @P@ is true for a list whenever it is true for the tail of the list,
+--   then @P@ is true.
+listInduction :: Proof (IsList xs) -> Proof (p Nil') -> Proof (ForAll ys ((IsList ys && p (Tail ys)) --> p ys)) -> Proof (p xs)
+listInduction _ _ _ = axiom
+
+consIsList :: Proof (IsCons xs) -> Proof (IsList xs)
+consIsList _ = axiom
+
+nilIsList :: Proof (IsNil xs) -> Proof (IsList xs)
+nilIsList _ = axiom
+
+listIsList :: ([a] ~~ xs) -> Proof (IsList xs)
+listIsList _ = axiom
diff --git a/src/Theory/Named.hs b/src/Theory/Named.hs
--- a/src/Theory/Named.hs
+++ b/src/Theory/Named.hs
@@ -4,6 +4,8 @@
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE RoleAnnotations       #-}
 
 {-|
   Module      :  Theory.Named
@@ -36,6 +38,7 @@
 --   representation as a value of type @a@, with a
 --   phantom "name" attached.
 newtype Named name a = Named a
+type role Named nominal nominal
 
 -- | An infix alias for 'Named'.
 type a ~~ name = Named name a
@@ -63,13 +66,23 @@
 {-| Library authors can introduce new names in a controlled way
     by creating @newtype@ wrappers of @Defn@. The constructor of
     the @newtype@ should *not* be exported, so that the library
-    can retain control of how the name is introduced.
+    can retain control of how the name is introduced. If a newtype
+    wrapper of @Defn@ contains phantom parameters, these parameters
+    should be given the @nominal@ type role; otherwise, library users
+    may be able to use coercions to manipulate library-specific names
+    in a manner not blessed by the library author.
 
 @
 newtype Bob = Bob Defn
 
 bob :: Int ~~ Bob
 bob = defn 42
+
+newtype FooOf name = FooOf Defn
+type role FooOf nominal -- disallow coerce :: FooOf name1 -> FooOf name2
+
+fooOf :: (Int ~~ name) -> (Int ~~ FooOf name)
+fooOf x = defn (the x)
 @
 -}
 data Defn = Defn