diff --git a/CHANGES.txt b/CHANGES.txt
new file mode 100644
--- /dev/null
+++ b/CHANGES.txt
@@ -0,0 +1,4 @@
+Changelog for QED
+
+0.0
+    Initial version
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Neil Mitchell 2015.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Neil Mitchell nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,5 @@
+# QED Prover [![Hackage version](https://img.shields.io/hackage/v/qed.svg?label=Hackage)](https://hackage.haskell.org/package/qed) [![Build Status](https://img.shields.io/travis/ndmitchell/qed.svg)](https://travis-ci.org/ndmitchell/qed)
+
+Experiments writing a proof system, particularly designed to prove properties about Haskell code, such as the [HLint rewrite rules](https://github.com/ndmitchell/hlint/blob/master/data/Default.hs).
+
+Tom Ellis described the approach as "coinduction on the execution".
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/imports/Builtin.hs b/imports/Builtin.hs
new file mode 100644
--- /dev/null
+++ b/imports/Builtin.hs
@@ -0,0 +1,15 @@
+module Builtin where
+
+error x = bottom
+
+bottom = bottom
+
+
+-- | The Monoid that is lawful, normalising, but no more
+(<>) = (++)
+mempty = []
+
+newtype Identity a = Identity a
+
+return = Identity
+a >>= b = case a of Identity a -> b a
diff --git a/imports/List.hs b/imports/List.hs
new file mode 100644
--- /dev/null
+++ b/imports/List.hs
@@ -0,0 +1,223 @@
+module List ( 
+    elemIndex, elemIndices,
+    find, findIndex, findIndices,
+    nub, nubBy, delete, deleteBy, (\\), deleteFirstsBy,
+    union, unionBy, intersect, intersectBy,
+    intersperse, transpose, partition, group, groupBy,
+    inits, tails, isPrefixOf, isSuffixOf,
+    mapAccumL, mapAccumR,
+    sort, sortBy, insert, insertBy, maximumBy, minimumBy,
+    genericLength, genericTake, genericDrop,
+    genericSplitAt, genericIndex, genericReplicate,
+    zip4, zip5, zip6, zip7,
+    zipWith4, zipWith5, zipWith6, zipWith7,
+    unzip4, unzip5, unzip6, unzip7, unfoldr,
+
+    -- ...and what the Prelude exports
+    -- []((:), []), -- This is built-in syntax
+    map, (++), concat, filter,
+    head, last, tail, init, null, length, (!!),
+    foldl, foldl1, scanl, scanl1, foldr, foldr1, scanr, scanr1,
+    iterate, repeat, replicate, cycle,
+    take, drop, splitAt, takeWhile, dropWhile, span, break,
+    lines, words, unlines, unwords, reverse, and, or,
+    any, all, elem, notElem, lookup,
+    sum, product, maximum, minimum, concatMap, 
+    zip, zip3, zipWith, zipWith3, unzip, unzip3
+    ) where
+
+import Maybe( listToMaybe )
+
+instance Monoid a where
+  mempty = []
+  mappend = (++)
+
+infix 5 \\
+
+elemIndex               :: Eq a => a -> [a] -> Maybe Int
+elemIndex x             =  findIndex (x ==)
+        
+elemIndices             :: Eq a => a -> [a] -> [Int]
+elemIndices x           =  findIndices (x ==)
+                        
+find                    :: (a -> Bool) -> [a] -> Maybe a
+find p                  =  listToMaybe . filter p
+
+findIndex               :: (a -> Bool) -> [a] -> Maybe Int
+findIndex p             =  listToMaybe . findIndices p
+
+findIndices             :: (a -> Bool) -> [a] -> [Int]
+findIndices p xs        =  [ i | (x,i) <- zip xs [0..], p x ]
+
+nub                     :: Eq a => [a] -> [a]
+nub                     =  nubBy (==)
+
+nubBy                   :: (a -> a -> Bool) -> [a] -> [a]
+nubBy eq x = case x of
+  []             ->  []
+  (x:xs)         ->  x : nubBy eq (filter (\y -> not (eq x y)) xs)
+
+delete                  :: Eq a => a -> [a] -> [a]
+delete                  =  deleteBy (==)
+
+deleteBy                :: (a -> a -> Bool) -> a -> [a] -> [a]
+deleteBy eq x ys = case ys of
+  []        -> []
+  (y:ys)    -> if x `eq` y then ys else y : deleteBy eq x ys
+
+(\\)                    :: Eq a => [a] -> [a] -> [a]
+(\\)                    =  foldl (flip delete)
+
+deleteFirstsBy          :: (a -> a -> Bool) -> [a] -> [a] -> [a]
+deleteFirstsBy eq       =  foldl (flip (deleteBy eq))
+
+union                   :: Eq a => [a] -> [a] -> [a]
+union                   =  unionBy (==)    
+
+unionBy                 :: (a -> a -> Bool) -> [a] -> [a] -> [a]
+unionBy eq xs ys        =  xs ++ deleteFirstsBy eq (nubBy eq ys) xs
+
+intersect               :: Eq a => [a] -> [a] -> [a]
+intersect               =  intersectBy (==)
+
+intersectBy             :: (a -> a -> Bool) -> [a] -> [a] -> [a]
+intersectBy eq xs ys    =  [x | x <- xs, any (eq x) ys]
+
+intersperse             :: a -> [a] -> [a]
+intersperse sep xs = case xs of
+  []      ->  []
+  x:xs -> case xs of
+    [] -> [x]
+    _:_ -> x : sep : intersperse sep xs
+
+-- transpose is lazy in both rows and columns,
+--       and works for non-rectangular 'matrices'
+-- For example, transpose [[1,2],[3,4,5],[]]  =  [[1,3],[2,4],[5]]
+-- Note that [h | (h:t) <- xss] is not the same as (map head xss)
+--      because the former discards empty sublists inside xss
+transpose                :: [[a]] -> [[a]]
+transpose xs = case xs of
+  []             -> []
+  x:xss -> case x of
+    [] ->  transpose xss
+    (x:xs) -> (x : [h | (h:t) <- xss]) : 
+                           transpose (xs : [t | (h:t) <- xss])
+
+partition               :: (a -> Bool) -> [a] -> ([a],[a])
+partition p xs          =  (filter p xs, filter (not . p) xs)
+
+-- group splits its list argument into a list of lists of equal, adjacent
+-- elements.  e.g.,
+-- group "Mississippi" == ["M","i","ss","i","ss","i","pp","i"]
+group                   :: Eq a => [a] -> [[a]]
+group                   =  groupBy (==)
+
+groupBy                 :: (a -> a -> Bool) -> [a] -> [[a]]
+groupBy eq xs = case xs of
+  []           ->  []
+  (x:xs)       ->  let o = span (eq x) xs in (x:fst o) : groupBy eq (snd o)
+
+-- inits xs returns the list of initial segments of xs, shortest first.
+-- e.g., inits "abc" == ["","a","ab","abc"]
+inits                   :: [a] -> [[a]]
+inits xs = case xs of
+  []                ->  [[]]
+  (x:xs)            ->  [[]] ++ map (x:) (inits xs)
+
+-- tails xs returns the list of all final segments of xs, longest first.
+-- e.g., tails "abc" == ["abc", "bc", "c",""]
+tails                   :: [a] -> [[a]]
+tails xxs = case xxs of
+  []                ->  [[]]
+  (_:xs)        ->  xxs : tails xs
+
+isPrefixOf               :: Eq a => [a] -> [a] -> Bool
+isPrefixOf xs ys = case xs of
+  []     -> True
+  x:xs -> case ys of
+    [] -> False
+    y:ys -> x == y && isPrefixOf xs ys
+
+isSuffixOf              :: Eq a => [a] -> [a] -> Bool
+isSuffixOf x y          =  reverse x `isPrefixOf` reverse y
+
+mapAccumL               :: (a -> b -> (a, c)) -> a -> [b] -> (a, [c])
+mapAccumL f s xs = case xs of
+  []        ->  (s, [])
+  (x:xs)    ->
+      let s'_y = f s x in
+      let s''_ys = mapAccumL f (fst s'_y) xs in
+      (fst s''_ys, snd s'_y : snd s''_ys)
+
+mapAccumR               :: (a -> b -> (a, c)) -> a -> [b] -> (a, [c])
+mapAccumR f s xs = case xs of
+  []        ->  (s, [])
+  (x:xs)    -> 
+      let s'_ys = mapAccumR f s xs in
+      let s''_y = f (fst s'_ys) x in
+      (fst s''_y, snd s''_y:snd s''_ys)
+
+unfoldr                 :: (b -> Maybe (a,b)) -> b -> [a]
+unfoldr f b             = case f b of
+                                Nothing    -> []
+                                Just ab -> case ab of (a,b) -> a : unfoldr f b
+
+sort                    :: (Ord a) => [a] -> [a]
+sort                    =  sortBy compare
+
+sortBy                  :: (a -> a -> Ordering) -> [a] -> [a]
+sortBy cmp              =  foldr (insertBy cmp) []
+
+insert                  :: (Ord a) => a -> [a] -> [a]
+insert                  = insertBy compare
+
+insertBy                :: (a -> a -> Ordering) -> a -> [a] -> [a]
+insertBy cmp x xs = case ys of
+    []       ->  [x]
+    y:ys' -> case cmp x y of
+        GT -> y : insertBy cmp x ys'
+        EQ  -> x : ys
+        LT  -> x : ys
+
+maximumBy               :: (a -> a -> Ordering) -> [a] -> a
+maximumBy cmp xs = case xs of
+ []        ->  error "List.maximumBy: empty list"
+ _:_ -> foldl1 (\x y -> case cmp x y of GT -> x; EQ -> y; LT -> y) xs
+
+minimumBy               :: (a -> a -> Ordering) -> [a] -> a
+minimumBy cmp xs = case xs of
+  []        ->  error "List.minimumBy: empty list"
+  _:_ -> foldl1 (\x y -> case cmp x y of GT -> y; EQ -> x; LT -> x) xs
+
+genericLength           :: (Integral a) => [b] -> a
+genericLength xs = case xs of
+  []        ->  0
+  (x:xs)    ->  1 + genericLength xs
+
+genericTake             :: (Integral a) => a -> [b] -> [b]
+genericTake n xs = case xs of
+  [] -> []
+  x:xs -> if n == 0 then []
+          else if n > 0 then x : genericTake (n-1) xs
+          else error "List.genericTake: negative argument"
+
+genericDrop             :: (Integral a) => a -> [b] -> [b]
+genericDrop n xs = if n == 0 then xs else case xs of
+  [] -> []
+  _:xs -> if n > 0 then genericDrop (n-1) xs else error "List.genericDrop: negative argument"
+
+genericSplitAt          :: (Integral a) => a -> [b] -> ([b],[b])
+genericSplitAt n xs = if n == 0 then ([],xs) else case xs of
+    [] -> ([],[])
+    x:xs -> let o = genericSplitAt (n-1) xs in
+            if n > 0 then (x:fst o, snd o) else error "List.genericSplitAt: negative argument"
+
+genericIndex            :: (Integral a) => [b] -> a -> b
+genericIndex xs n = case xs of
+  [] -> error "List.genericIndex: index too large"
+  x:xs -> if n == 0 then x
+          else if n > 0 then genericIndex xs (n-1)
+          else error "List.genericIndex: negative argument"
+
+genericReplicate        :: (Integral a) => a -> b -> [b]
+genericReplicate n x    =  genericTake n (repeat x)
diff --git a/imports/Maybe.hs b/imports/Maybe.hs
new file mode 100644
--- /dev/null
+++ b/imports/Maybe.hs
@@ -0,0 +1,56 @@
+
+module Maybe(
+    isJust, isNothing,
+    fromJust, fromMaybe, listToMaybe, maybeToList,
+    catMaybes, mapMaybe,
+
+    -- ...and what the Prelude exports
+    Maybe(Nothing, Just),
+    maybe
+  ) where
+
+instance Eq a => Eq (Maybe a) where
+    (==) = eqMaybe
+
+eqMaybe x y = case x of
+    Nothing -> case y of
+        Nothing -> True
+        Just _ -> False
+    Just x -> case y of
+        Nothing -> False
+        Just y -> x == y
+
+isJust                 :: Maybe a -> Bool
+isJust x = case x of
+    (Just a)        -> True
+    Nothing         ->  False
+
+isNothing          :: Maybe a -> Bool
+isNothing          =  not . isJust
+
+fromJust               :: Maybe a -> a
+fromJust x = case x of
+    (Just a)      ->  a
+    Nothing       ->  error "Maybe.fromJust: Nothing"
+
+fromMaybe              :: a -> Maybe a -> a
+fromMaybe d x = case x of
+    Nothing    ->  d
+    Just a      ->  a
+
+maybeToList            :: Maybe a -> [a]
+maybeToList x = case x of
+    Nothing -> []
+    Just a -> [a]
+
+listToMaybe            :: [a] -> Maybe a
+listToMaybe = case x of
+    []         ->  Nothing
+    (a:_)      ->  Just a
+ 
+catMaybes              :: [Maybe a] -> [a]
+catMaybes ms           =  [ m | Just m <- ms ]
+-- concatMap (\x -> case x of Nothing -> []; Just m -> [m]) ms
+
+mapMaybe               :: (a -> Maybe b) -> [a] -> [b]
+mapMaybe f             =  catMaybes . map f
diff --git a/imports/Monad.hs b/imports/Monad.hs
new file mode 100644
--- /dev/null
+++ b/imports/Monad.hs
@@ -0,0 +1,86 @@
+module Monad (
+    MonadPlus(mzero, mplus),
+    join, guard, when, unless, ap,
+    msum,
+    filterM, mapAndUnzipM, zipWithM, zipWithM_, foldM, 
+    liftM, liftM2, liftM3, liftM4, liftM5,
+
+    -- ...and what the Prelude exports
+    Monad((>>=), (>>), return, fail),
+    Functor(fmap),
+    mapM, mapM_, sequence, sequence_, (=<<), 
+    ) where
+
+
+-- The MonadPlus class definition
+
+class  (Monad m) => MonadPlus m  where
+    mzero  :: m a
+    mplus  :: m a -> m a -> m a
+
+
+-- Instances of MonadPlus
+
+instance  MonadPlus Maybe  where
+    mzero                 = Nothing
+
+    Nothing `mplus` ys    =  ys
+    xs      `mplus` ys    =  xs
+
+instance  MonadPlus []  where
+    mzero =  []
+    mplus = (++)
+
+
+-- Functions    
+
+
+msum   :: MonadPlus m => [m a] -> m a
+msum xs  =  foldr mplus mzero xs
+
+join             :: (Monad m) => m (m a) -> m a
+join x           =  x >>= id
+
+when             :: (Monad m) => Bool -> m () -> m ()
+when p s         =  if p then s else return ()
+
+unless           :: (Monad m) => Bool -> m () -> m ()
+unless p s       =  when (not p) s
+
+ap               :: (Monad m) => m (a -> b) -> m a -> m b
+ap               =  liftM2 ($)
+
+guard            :: MonadPlus m => Bool -> m ()
+guard p          =  if p then return () else mzero
+
+mapAndUnzipM     :: (Monad m) => (a -> m (b,c)) -> [a] -> m ([b], [c])
+mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip
+
+zipWithM         :: (Monad m) => (a -> b -> m c) -> [a] -> [b] -> m [c]
+zipWithM f xs ys =  sequence (zipWith f xs ys)
+
+zipWithM_         :: (Monad m) => (a -> b -> m c) -> [a] -> [b] -> m ()
+zipWithM_ f xs ys =  sequence_ (zipWith f xs ys)
+
+foldM            :: (Monad m) => (a -> b -> m a) -> a -> [b] -> m a
+foldM f a xs = case xs of
+  [] -> return a
+  x:xs -> f a x >>= \ y -> foldM f y xs
+
+filterM :: Monad m => (a -> m Bool) -> [a] -> m [a]
+filterM p xs = case xs of
+  [] -> return []
+  x:xs ->
+      p x >>= \b ->
+      filterM p xs >>= \ys ->
+      return (if b then (x:ys) else ys)
+
+liftM            :: (Monad m) => (a -> b) -> (m a -> m b)
+liftM f          =  \a -> a >>= \a' -> return (f a')
+
+liftM2           :: (Monad m) => (a -> b -> c) -> (m a -> m b -> m c)
+liftM2 f         =  \a b -> a >>= \a' -> b >>= \b' -> return (f a' b')
+
+liftM3           :: (Monad m) => (a -> b -> c -> d) ->
+                                 (m a -> m b -> m c -> m d)
+liftM3 f         =  \a b c -> a >>= \a' -> b >>= \b' -> c >>= \c' -> return (f a' b' c')
diff --git a/imports/Prelude.hs b/imports/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/imports/Prelude.hs
@@ -0,0 +1,1198 @@
+module Prelude (
+    module PreludeList, module PreludeText, module PreludeIO,
+    Bool(False, True),
+    Maybe(Nothing, Just),
+    Either(Left, Right),
+    Ordering(LT, EQ, GT),
+    Char, String, Int, Integer, Float, Double, Rational, IO,
+
+--      These built-in types are defined in the Prelude, but
+--      are denoted by built-in syntax, and cannot legally
+--      appear in an export list.
+--  List type: []((:), [])
+--  Tuple types: (,)((,)), (,,)((,,)), etc.
+--  Trivial type: ()(())
+--  Functions: (->)
+
+    Eq((==), (/=)),
+    Ord(compare, (<), (<=), (>=), (>), max, min),
+    Enum(succ, pred, toEnum, fromEnum, enumFrom, enumFromThen,
+         enumFromTo, enumFromThenTo),
+    Bounded(minBound, maxBound),
+    Num((+), (-), (*), negate, abs, signum, fromInteger),
+    Real(toRational),
+    Integral(quot, rem, div, mod, quotRem, divMod, toInteger),
+    Fractional((/), recip, fromRational),
+    Floating(pi, exp, log, sqrt, (**), logBase, sin, cos, tan,
+             asin, acos, atan, sinh, cosh, tanh, asinh, acosh, atanh),
+    RealFrac(properFraction, truncate, round, ceiling, floor),
+    RealFloat(floatRadix, floatDigits, floatRange, decodeFloat,
+              encodeFloat, exponent, significand, scaleFloat, isNaN,
+              isInfinite, isDenormalized, isIEEE, isNegativeZero, atan2),
+    Monad((>>=), (>>), return, fail),
+    Functor(fmap),
+    mapM, mapM_, sequence, sequence_, (=<<), 
+    maybe, either,
+    (&&), (||), not, otherwise,
+    subtract, even, odd, gcd, lcm, (^), (^^), 
+    fromIntegral, realToFrac, 
+    fst, snd, curry, uncurry, id, const, (.), flip, ($), until,
+    asTypeOf, error, undefined,
+    seq, ($!)
+  ) where
+
+import PreludeBuiltin                      -- Contains all `prim' values
+import UnicodePrims( primUnicodeMaxChar )  -- Unicode primitives
+import PreludeList
+import PreludeText
+import PreludeIO
+import Ratio( Rational )
+
+infixr 9  .
+infixr 8  ^, ^^, **
+infixl 7  *, /, `quot`, `rem`, `div`, `mod`
+infixl 6  +, -
+
+-- The (:) operator is built-in syntax, and cannot legally be given
+-- a fixity declaration; but its fixity is given by:
+--   infixr 5  :
+
+infix  4  ==, /=, <, <=, >=, >
+infixr 3  &&
+infixr 2  ||
+infixl 1  >>, >>=
+infixr 1  =<<
+infixr 0  $, $!, `seq`
+
+-- Standard types, classes, instances and related functions
+
+-- Equality and Ordered classes
+
+
+class  Eq a  where
+    (==), (/=) :: a -> a -> Bool
+
+        -- Minimal complete definition:
+        --      (==) or (/=)
+    x /= y     =  not (x == y)
+    x == y     =  not (x /= y)
+
+
+class  (Eq a) => Ord a  where
+    compare              :: a -> a -> Ordering
+    (<), (<=), (>=), (>) :: a -> a -> Bool
+    max, min             :: a -> a -> a
+
+        -- Minimal complete definition:
+        --      (<=) or compare
+        -- Using compare can be more efficient for complex types.
+    compare x y = if x == y then EQ else if x <= y then LT else GT
+
+    x <= y           =  compare x y /= GT
+    x <  y           =  compare x y == LT
+    x >= y           =  compare x y /= LT
+    x >  y           =  compare x y == GT
+
+-- note that (min x y, max x y) = (x,y) or (y,x)
+    max x y = if x <= y then y else x
+    min x y = if x <= y then x else y
+
+-- Enumeration and Bounded classes
+
+
+class  Enum a  where
+    succ, pred       :: a -> a
+    toEnum           :: Int -> a
+    fromEnum         :: a -> Int
+    enumFrom         :: a -> [a]             -- [n..]
+    enumFromThen     :: a -> a -> [a]        -- [n,n'..]
+    enumFromTo       :: a -> a -> [a]        -- [n..m]
+    enumFromThenTo   :: a -> a -> a -> [a]   -- [n,n'..m]
+
+        -- Minimal complete definition:
+        --      toEnum, fromEnum
+--
+-- NOTE: these default methods only make sense for types
+--   that map injectively into Int using fromEnum
+--   and toEnum.
+    succ             =  toEnum . (+1) . fromEnum
+    pred             =  toEnum . (subtract 1) . fromEnum
+    enumFrom x       =  map toEnum [fromEnum x ..]
+    enumFromTo x y   =  map toEnum [fromEnum x .. fromEnum y]
+    enumFromThen x y =  map toEnum [fromEnum x, fromEnum y ..]
+    enumFromThenTo x y z = 
+                        map toEnum [fromEnum x, fromEnum y .. fromEnum z]
+
+
+class  Bounded a  where
+    minBound         :: a
+    maxBound         :: a
+
+-- Numeric classes
+
+
+class  (Eq a, Show a) => Num a  where
+    (+), (-), (*)    :: a -> a -> a
+    negate           :: a -> a
+    abs, signum      :: a -> a
+    fromInteger      :: Integer -> a
+
+        -- Minimal complete definition:
+        --      All, except negate or (-)
+    x - y            =  x + negate y
+    negate x         =  0 - x
+
+
+class  (Num a, Ord a) => Real a  where
+    toRational       ::  a -> Rational
+
+
+class  (Real a, Enum a) => Integral a  where
+    quot, rem        :: a -> a -> a   
+    div, mod         :: a -> a -> a
+    quotRem, divMod  :: a -> a -> (a,a)
+    toInteger        :: a -> Integer
+
+        -- Minimal complete definition:
+        --      quotRem, toInteger
+    n `quot` d       =  fst $ quotRem n d
+    n `rem` d        =  snd $ quotRem n d
+    n `div` d        =  fst $ divMod n d
+    n `mod` d        =  snd $ divMod n d
+    divMod n d       =  if signum r == - signum d then (q-1, r+d) else qr
+                        where qr = quotRem n d
+                              q = fst qr
+                              r = snd qr
+
+
+class  (Num a) => Fractional a  where
+    (/)              :: a -> a -> a
+    recip            :: a -> a
+    fromRational     :: Rational -> a
+
+        -- Minimal complete definition:
+        --      fromRational and (recip or (/))
+    recip x          =  1 / x
+    x / y            =  x * recip y
+
+
+class  (Fractional a) => Floating a  where
+    pi                  :: a
+    exp, log, sqrt      :: a -> a
+    (**), logBase       :: a -> a -> a
+    sin, cos, tan       :: a -> a
+    asin, acos, atan    :: a -> a
+    sinh, cosh, tanh    :: a -> a
+    asinh, acosh, atanh :: a -> a
+
+        -- Minimal complete definition:
+        --      pi, exp, log, sin, cos, sinh, cosh
+        --      asin, acos, atan
+        --      asinh, acosh, atanh
+    x ** y           =  exp (log x * y)
+    logBase x y      =  log y / log x
+    sqrt x           =  x ** 0.5
+    tan  x           =  sin  x / cos  x
+    tanh x           =  sinh x / cosh x
+
+
+
+class  (Real a, Fractional a) => RealFrac a  where
+    properFraction   :: (Integral b) => a -> (b,a)
+    truncate, round  :: (Integral b) => a -> b
+    ceiling, floor   :: (Integral b) => a -> b
+
+        -- Minimal complete definition:
+        --      properFraction
+    truncate x       =  fst $ properFraction x
+    
+
+class  (RealFrac a, Floating a) => RealFloat a  where
+    floatRadix       :: a -> Integer
+    floatDigits      :: a -> Int
+    floatRange       :: a -> (Int,Int)
+    decodeFloat      :: a -> (Integer,Int)
+    encodeFloat      :: Integer -> Int -> a
+    exponent         :: a -> Int
+    significand      :: a -> a
+    scaleFloat       :: Int -> a -> a
+    isNaN, isInfinite, isDenormalized, isNegativeZero, isIEEE
+                     :: a -> Bool
+    atan2            :: a -> a -> a
+
+        -- Minimal complete definition:
+        --      All except exponent, significand, 
+        --                 scaleFloat, atan2
+-- Numeric functions
+
+
+subtract         :: (Num a) => a -> a -> a
+subtract         =  flip (-)
+
+
+even, odd        :: (Integral a) => a -> Bool
+even n           =  n `rem` 2 == 0
+odd              =  not . even
+
+
+
+
+fromIntegral     :: (Integral a, Num b) => a -> b
+fromIntegral     =  fromInteger . toInteger
+
+
+realToFrac     :: (Real a, Fractional b) => a -> b
+realToFrac      =  fromRational . toRational
+
+-- Monadic classes
+
+
+class  Functor f  where
+    fmap              :: (a -> b) -> f a -> f b
+
+
+class  Monad m  where
+    (>>=)  :: m a -> (a -> m b) -> m b
+    (>>)   :: m a -> m b -> m b
+    return :: a -> m a
+    fail   :: String -> m a
+
+        -- Minimal complete definition:
+        --      (>>=), return
+    m >> k  =  m >>= \_ -> k
+    fail s  = error s
+
+
+sequence       :: Monad m => [m a] -> m [a] 
+sequence       =  foldr (\p q -> p >>= \x -> q >>= \y -> return (x:y)) (return [])
+
+
+sequence_      :: Monad m => [m a] -> m () 
+sequence_      =  foldr (>>) (return ())
+
+-- The xxxM functions take list arguments, but lift the function or
+-- list element to a monad type
+
+mapM             :: Monad m => (a -> m b) -> [a] -> m [b]
+mapM f as        =  sequence (map f as)
+
+
+mapM_            :: Monad m => (a -> m b) -> [a] -> m ()
+mapM_ f as       =  sequence_ (map f as)
+
+
+(=<<)            :: Monad m => (a -> m b) -> m a -> m b
+f =<< x          =  x >>= f
+
+
+-- Trivial type
+
+
+-- data  ()  =  ()  deriving (Eq, Ord, Enum, Bounded)
+-- Not legal Haskell; for illustration only
+
+-- Function type
+
+-- identity function
+
+id               :: a -> a
+id x             =  x
+
+-- constant function
+
+const            :: a -> b -> a
+const x y        =  x
+
+-- function composition
+
+(.)              :: (b -> c) -> (a -> b) -> a -> c
+f . g            =  \ x -> f (g x)
+
+-- flip f  takes its (first) two arguments in the reverse order of f.
+
+flip             :: (a -> b -> c) -> b -> a -> c
+flip f x y       =  f y x
+
+
+seq :: a -> b -> b
+seq = ...       -- Primitive
+
+-- right-associating infix application operators 
+-- (useful in continuation-passing style)
+
+($), ($!) :: (a -> b) -> a -> b
+f $  x    =  f x
+f $! x    =  x `seq` f x
+
+
+-- Boolean type
+
+
+data  Bool  =  False | True     deriving (Eq, Ord, Enum, Read, Show, Bounded)
+
+-- Boolean functions
+
+
+(&&), (||)       :: Bool -> Bool -> Bool
+x && y = case x of True -> y; False -> False
+x || y = case x of True -> True; False -> y
+
+not              :: Bool -> Bool
+not x = case x of True -> False; False -> True
+
+
+otherwise        :: Bool
+otherwise        =  True
+
+
+-- Character type
+
+
+-- data Char = ... 'a' | 'b' ... -- Unicode values
+
+
+instance  Eq Char  where
+    c == c'          =  fromEnum c == fromEnum c'
+
+
+instance  Ord Char  where
+    c <= c'          =  fromEnum c <= fromEnum c'
+
+
+instance  Enum Char  where
+    toEnum            = primIntToChar
+    fromEnum          = primCharToInt
+    enumFrom c        = map toEnum [fromEnum c .. fromEnum (maxBound::Char)]
+    enumFromThen c c' = map toEnum [fromEnum c, fromEnum c' .. fromEnum lastChar]
+                      where lastChar :: Char
+                            lastChar | c' < c    = minBound
+                                     | otherwise = maxBound
+
+
+instance  Bounded Char  where
+    minBound  =  '\0'
+    maxBound  =  primUnicodeMaxChar
+
+
+type  String = [Char]
+
+
+-- Maybe type
+
+
+data  Maybe a  =  Nothing | Just a      deriving (Eq, Ord, Read, Show)
+
+
+maybe              :: b -> (a -> b) -> Maybe a -> b
+maybe n f x = case x of Nothing -> n; Just x ->  f x
+
+
+instance  Functor Maybe  where
+    fmap f Nothing    =  Nothing
+    fmap f (Just x)   =  Just (f x)
+        
+
+instance  Monad Maybe  where
+    (Just x) >>= k   =  k x
+    Nothing  >>= k   =  Nothing
+    return           =  Just
+    fail s           =  Nothing
+
+-- Either type
+
+
+data  Either a b  =  Left a | Right b   deriving (Eq, Ord, Read, Show)
+
+
+either               :: (a -> c) -> (b -> c) -> Either a b -> c
+either f g x = case x of Left x -> f x; Right y ->  g y
+
+-- IO type
+
+
+data IO a     -- abstract
+
+
+instance  Functor IO where
+   fmap f x           =  x >>= (return . f)
+
+
+instance Monad IO where
+   (>>=)  = ...
+   return = ...
+   fail s = ioError (userError s)
+
+-- Ordering type
+
+
+data  Ordering  =  LT | EQ | GT
+          deriving (Eq, Ord, Enum, Read, Show, Bounded)
+
+
+-- Standard numeric types.  The data declarations for these types cannot
+-- be expressed directly in Haskell since the constructor lists would be
+-- far too large.
+
+
+data  Int 
+
+instance  Eq       Int  where 
+
+instance  Ord      Int  where 
+
+instance  Num      Int  where 
+
+instance  Real     Int  where 
+
+instance  Integral Int  where 
+
+instance  Enum     Int  where 
+
+instance  Bounded  Int  where 
+
+
+data  Integer  
+
+instance  Eq       Integer  where 
+
+instance  Ord      Integer  where
+
+instance  Num      Integer  where
+
+instance  Real     Integer  where
+
+instance  Integral Integer  where
+
+instance  Enum     Integer  where
+
+
+data  Float
+
+instance  Eq         Float  where
+
+instance  Ord        Float  where
+
+instance  Num        Float  where
+
+instance  Real       Float  where
+
+instance  Fractional Float  where
+
+instance  Floating   Float  where
+
+instance  RealFrac   Float  where
+
+instance  RealFloat  Float  where
+
+
+data  Double
+
+instance  Eq         Double  where
+
+instance  Ord        Double  where
+
+instance  Num        Double  where
+
+instance  Real       Double  where
+
+instance  Fractional Double  where
+
+instance  Floating   Double  where
+
+instance  RealFrac   Double  where
+
+instance  RealFloat  Double  where
+
+-- The Enum instances for Floats and Doubles are slightly unusual.
+-- The `toEnum' function truncates numbers to Int.  The definitions
+-- of enumFrom and enumFromThen allow floats to be used in arithmetic
+-- series: [0,0.1 .. 0.95].  However, roundoff errors make these somewhat
+-- dubious.  This example may have either 10 or 11 elements, depending on
+-- how 0.1 is represented.
+
+
+instance  Enum Float  where
+    succ x           =  x+1
+    pred x           =  x-1
+    toEnum           =  fromIntegral
+    fromEnum         =  fromInteger . truncate   -- may overflow
+    enumFrom         =  numericEnumFrom
+    enumFromThen     =  numericEnumFromThen
+    enumFromTo       =  numericEnumFromTo
+    enumFromThenTo   =  numericEnumFromThenTo
+
+
+instance  Enum Double  where
+    succ x           =  x+1
+    pred x           =  x-1
+    toEnum           =  fromIntegral
+    fromEnum         =  fromInteger . truncate   -- may overflow
+    enumFrom         =  numericEnumFrom
+    enumFromThen     =  numericEnumFromThen
+    enumFromTo       =  numericEnumFromTo
+    enumFromThenTo   =  numericEnumFromThenTo
+
+
+numericEnumFrom         :: (Fractional a) => a -> [a]
+
+numericEnumFromThen     :: (Fractional a) => a -> a -> [a]
+
+numericEnumFromTo       :: (Fractional a, Ord a) => a -> a -> [a]
+
+numericEnumFromThenTo   :: (Fractional a, Ord a) => a -> a -> a -> [a]
+numericEnumFrom         =  iterate (+1)
+numericEnumFromThen n m =  iterate (+(m-n)) n
+numericEnumFromTo n m   =  takeWhile (<= m+1/2) (numericEnumFrom n)
+numericEnumFromThenTo n n' m = takeWhile p (numericEnumFromThen n n')
+                             where
+                               p = if n' >= n then (<= m + (n'-n)/2) else (>= m + (n'-n)/2)
+
+-- Lists
+
+
+-- data  [a]  =  [] | a : [a]  deriving (Eq, Ord)
+-- Not legal Haskell; for illustration only
+
+
+instance Functor [] where
+    fmap = map
+
+
+instance  Monad []  where
+    m >>= k          = concat (map k m)
+    return x         = [x]
+    fail s           = []
+
+-- Tuples
+
+
+--data  (a,b)   =  (a,b)    deriving (Eq, Ord, Bounded)
+
+--data  (a,b,c) =  (a,b,c)  deriving (Eq, Ord, Bounded)
+-- Not legal Haskell; for illustration only
+
+-- component projections for pairs:
+-- (NB: not provided for triples, quadruples, etc.)
+
+fst              :: (a,b) -> a
+fst (x,y)        =  x
+
+
+snd              :: (a,b) -> b
+snd (x,y)        =  y
+
+-- curry converts an uncurried function to a curried function;
+-- uncurry converts a curried function to a function on pairs.
+
+curry            :: ((a, b) -> c) -> a -> b -> c
+curry f x y      =  f (x, y)
+
+
+uncurry          :: (a -> b -> c) -> ((a, b) -> c)
+uncurry f p      =  f (fst p) (snd p)
+
+-- Misc functions
+
+-- until p f  yields the result of applying f until p holds.
+
+until            :: (a -> Bool) -> (a -> a) -> a -> a
+until p f x = if p x then x else until p f (f x)
+
+-- asTypeOf is a type-restricted version of const.  It is usually used
+-- as an infix operator, and its typing forces its first argument
+-- (which is usually overloaded) to have the same type as the second.
+
+asTypeOf         :: a -> a -> a
+asTypeOf         =  const
+
+-- error stops execution and displays an error message
+
+
+error            :: String -> a
+error            =  primError
+
+-- It is expected that compilers will recognize this and insert error
+-- messages that are more appropriate to the context in which undefined 
+-- appears. 
+
+
+undefined        :: a
+undefined        =  error "Prelude.undefined"
+
+
+infixl 9  !!
+infixr 5  ++
+infix  4  `elem`, `notElem`
+
+-- Map and append
+
+map :: (a -> b) -> [a] -> [b]
+map f x = case x of [] -> []; (x:xs) -> f x : map f xs
+
+
+(++) :: [a] -> [a] -> [a]
+xs ++ ys = case xs of [] -> ys; (x:xs) -> x : (xs ++ ys)
+
+
+filter :: (a -> Bool) -> [a] -> [a]
+filter p xs = case xs of
+     [] -> []
+     x:xs -> if p x then x : filter p xs else  filter p xs
+
+
+concat :: [[a]] -> [a]
+concat xss = foldr (++) [] xss
+
+
+concatMap :: (a -> [b]) -> [a] -> [b]
+concatMap f = concat . map f
+
+-- head and tail extract the first element and remaining elements,
+-- respectively, of a list, which must be non-empty.  last and init
+-- are the dual functions working from the end of a finite list,
+-- rather than the beginning.
+
+
+head             :: [a] -> a
+head x = case x of
+    (x:_)       ->  x
+    []          ->  error "Prelude.head: empty list"
+
+
+tail             :: [a] -> [a]
+tail x = case x of
+    (_:xs)      -> xs
+    []          ->  error "Prelude.tail: empty list"
+
+
+last             :: [a] -> a
+last x = case x of
+    [] -> error "Prelude.last: empty list"
+    x:xs -> case xs of
+        [] -> x
+        _:_ -> last xs
+
+
+init             :: [a] -> [a]
+init x = case x of
+    [] -> error "Prelude.init: empty list"
+    x:xs -> case xs of
+        [] -> []
+        _:_ -> x : init xs
+
+
+null             :: [a] -> Bool
+null x = case x of [] -> True; (_:_) ->  False
+
+-- length returns the length of a finite list as an Int.
+
+length           :: [a] -> Int
+length xs = case xs of
+    [] -> 0
+    _:l -> 1 + length l
+
+-- List index (subscript) operator, 0-origin
+
+(!!)                :: [a] -> Int -> a
+(!!) xs n = if n < 0 then error "Prelude.!!: negative index"
+       else case x of
+                [] -> error "Prelude.!!: index too large"
+                x:xs -> if n == 0 then x else xs !! (n-1)
+
+-- foldl, applied to a binary operator, a starting value (typically the
+-- left-identity of the operator), and a list, reduces the list using
+-- the binary operator, from left to right:
+--  foldl f z [x1, x2, ..., xn] == (...((z `f` x1) `f` x2) `f`...) `f` xn
+-- foldl1 is a variant that has no starting value argument, and  thus must
+-- be applied to non-empty lists.  scanl is similar to foldl, but returns
+-- a list of successive reduced values from the left:
+--      scanl f z [x1, x2, ...] == [z, z `f` x1, (z `f` x1) `f` x2, ...]
+-- Note that  last (scanl f z xs) == foldl f z xs.
+-- scanl1 is similar, again without the starting element:
+--      scanl1 f [x1, x2, ...] == [x1, x1 `f` x2, ...]
+
+
+foldl            :: (a -> b -> a) -> a -> [b] -> a
+foldl f z x = case x of
+    []     ->  z
+    (x:xs) ->  foldl f (f z x) xs
+
+
+foldl1           :: (a -> a -> a) -> [a] -> a
+foldl1 f x = case x of
+    [] -> error "Prelude.foldl1: empty list"
+    (x:xs)  ->  foldl f x xs
+
+
+scanl            :: (a -> b -> a) -> a -> [b] -> [a]
+scanl f q xs     =  q : (case xs of
+                            []   -> []
+                            x:xs -> scanl f (f q x) xs)
+
+
+scanl1           :: (a -> a -> a) -> [a] -> [a]
+scanl1 f x = case x of
+    [] -> []
+    (x:xs)  ->  scanl f x xs
+
+-- foldr, foldr1, scanr, and scanr1 are the right-to-left duals of the
+-- above functions.
+
+
+foldr            :: (a -> b -> b) -> b -> [a] -> b
+foldr f z x = case x of
+    []     ->  z
+    (x:xs) ->  f x (foldr f z xs)
+
+
+foldr1           :: (a -> a -> a) -> [a] -> a
+foldr1 f x = case x of
+    [] -> error "Prelude.foldr1: empty list"
+    x:xs -> case xs of
+        [] -> x
+        _:_ -> f x (foldr1 f xs)
+
+
+scanr             :: (a -> b -> b) -> b -> [a] -> [b]
+scanr f q0 x = case x of
+    []     ->  [q0]
+    (x:xs) -> let qs = scanr f q0 xs in f x (head qs) : qs
+
+scanr1          :: (a -> a -> a) -> [a] -> [a]
+scanr1 f x = case x of
+    []     ->  []
+    x:xs   -> case xs of
+        [] -> [x]
+        _:_ -> let qs = scanr1 f xs in f x (head qs) : qs
+
+-- iterate f x returns an infinite list of repeated applications of f to x:
+-- iterate f x == [x, f x, f (f x), ...]
+
+iterate          :: (a -> a) -> a -> [a]
+iterate f x      =  x : iterate f (f x)
+
+-- repeat x is an infinite list, with x the value of every element.
+
+repeat           :: a -> [a]
+repeat x         =  x : repeat x
+
+-- replicate n x is a list of length n with x the value of every element
+
+replicate        :: Int -> a -> [a]
+replicate n x    =  take n (repeat x)
+
+-- cycle ties a finite list into a circular one, or equivalently,
+-- the infinite repetition of the original list.  It is the identity
+-- on infinite lists.
+
+
+cycle            :: [a] -> [a]
+cycle xs = case xs of
+    []         ->  error "Prelude.cycle: empty list"
+    _:_    -> xs ++ cycle xs
+
+-- take n, applied to a list xs, returns the prefix of xs of length n,
+-- or xs itself if n > length xs.  drop n xs returns the suffix of xs
+-- after the first n elements, or [] if n > length xs.  splitAt n xs
+-- is equivalent to (take n xs, drop n xs).
+
+
+take                   :: Int -> [a] -> [a]
+take n xs = if n <= 0 then  []
+            else case xs of
+                    [] -> []
+                    x:xs -> x : take (n-1) xs
+
+
+drop                   :: Int -> [a] -> [a]
+drop n xs = if n <= 0 then xs
+            else case xs of
+                     [] -> []
+                     x:xs -> drop (n-1) xs
+
+
+splitAt                  :: Int -> [a] -> ([a],[a])
+splitAt n xs             =  (take n xs, drop n xs)
+
+-- takeWhile, applied to a predicate p and a list xs, returns the longest
+-- prefix (possibly empty) of xs of elements that satisfy p.  dropWhile p xs
+-- returns the remaining suffix.  span p xs is equivalent to 
+-- (takeWhile p xs, dropWhile p xs), while break p uses the negation of p.
+
+
+takeWhile               :: (a -> Bool) -> [a] -> [a]
+takeWhile p xs = case xs of
+    []          ->  []
+    x:xs        -> if p x then  x : takeWhile p xs else []
+
+
+dropWhile               :: (a -> Bool) -> [a] -> [a]
+dropWhile p xs = case xs of
+    []          ->  []
+    x:xs' -> if p x then  dropWhile p xs' else  xs
+
+
+span, break             :: (a -> Bool) -> [a] -> ([a],[a])
+span p xs = case xs of
+    []            -> ([],[])
+    x:xs'  -> let ys_zs = span p xs'
+              in if p x then (x:fst ys_zs, snd ys_zs)
+                        else ([],xs)
+
+break p                 =  span (not . p)
+
+-- lines breaks a string up into a list of strings at newline characters.
+-- The resulting strings do not contain newlines.  Similary, words
+-- breaks a string up into a list of words, which were delimited by
+-- white space.  unlines and unwords are the inverse operations.
+-- unlines joins lines with terminating newlines, and unwords joins
+-- words with separating spaces.
+
+
+lines            :: String -> [String]
+lines s          =  if null s then [] else let ls = break (== '\n') s
+                      in  fst ls : case snd ls of
+                                []      -> []
+                                (_:s'') -> lines s''
+
+
+words            :: String -> [String]
+words s          =  let s' = dropWhile isSpace s  in
+                    case s' of
+                      [] -> []
+                      _:_ -> let ws = break isSpace s' in
+                             fst ws : words (snd ws)
+
+
+unlines          :: [String] -> String
+unlines          =  concatMap (++ "\n")
+
+
+unwords          :: [String] -> String
+unwords ws = case ws of
+     []       ->  ""
+     _:_ -> foldr1 (\w s -> w ++ ' ':s) ws
+
+-- reverse xs returns the elements of xs in reverse order.  xs must be finite.
+
+reverse          :: [a] -> [a]
+reverse          =  foldl (flip (:)) []
+
+-- and returns the conjunction of a Boolean list.  For the result to be
+-- True, the list must be finite; False, however, results from a False
+-- value at a finite index of a finite or infinite list.  or is the
+-- disjunctive dual of and.
+
+and, or          :: [Bool] -> Bool
+and              =  foldr (&&) True
+or               =  foldr (||) False
+
+-- Applied to a predicate and a list, any determines if any element
+-- of the list satisfies the predicate.  Similarly, for all.
+
+any, all         :: (a -> Bool) -> [a] -> Bool
+any p            =  or . map p
+all p            =  and . map p
+
+-- elem is the list membership predicate, usually written in infix form,
+-- e.g., x `elem` xs.  notElem is the negation.
+
+elem, notElem    :: (Eq a) => a -> [a] -> Bool
+elem x           =  any (== x)
+notElem x        =  all (/= x)
+
+-- lookup key assocs looks up a key in an association list.
+
+lookup           :: (Eq a) => a -> [(a,b)] -> Maybe b
+lookup key xs = case xs of
+    [] -> Nothing
+    xy:xys -> case xy of
+        (x,y) -> if key == x then Just y else lookup key xys
+
+-- sum and product compute the sum or product of a finite list of numbers.
+
+sum, product     :: (Num a) => [a] -> a
+sum              =  foldl (+) 0  
+product          =  foldl (*) 1
+
+-- maximum and minimum return the maximum or minimum value from a list,
+-- which must be non-empty, finite, and of an ordered type.
+
+maximum, minimum :: (Ord a) => [a] -> a
+maximum xs = case xs of
+    [] -> error "Prelude.maximum: empty list"
+    _:_ -> foldl1 max xs
+
+minimum xs = case xs of
+    [] ->  error "Prelude.minimum: empty list"
+    _:_ -> foldl1 min xs
+
+-- zip takes two lists and returns a list of corresponding pairs.  If one
+-- input list is short, excess elements of the longer list are discarded.
+-- zip3 takes three lists and returns a list of triples.  Zips for larger
+-- tuples are in the List library
+
+
+zip              :: [a] -> [b] -> [(a,b)]
+zip              =  zipWith (,)
+
+
+zip3             :: [a] -> [b] -> [c] -> [(a,b,c)]
+zip3             =  zipWith3 (,,)
+
+-- The zipWith family generalises the zip family by zipping with the
+-- function given as the first argument, instead of a tupling function.
+-- For example, zipWith (+) is applied to two lists to produce the list
+-- of corresponding sums.
+
+
+zipWith          :: (a->b->c) -> [a]->[b]->[c]
+zipWith z as bs =
+    case as of
+        [] -> []
+        a:as -> case bs of
+            [] -> []
+            b:bs -> z a b : zipWith z as bs
+
+
+zipWith3         :: (a->b->c->d) -> [a]->[b]->[c]->[d]
+zipWith3 z as bs cs = case as of
+    [] -> []
+    a:as -> case bs of
+        [] -> []
+        b:bs -> case cs of
+            [] -> []
+            c:cs -> z a b c : zipWith3 z as bs cs
+
+
+-- unzip transforms a list of pairs into a pair of lists.  
+
+
+unzip            :: [(a,b)] -> ([a],[b])
+unzip            =  foldr (\ab asbs -> case ab of (a,b) -> (a:fst asbs,b:snd asbs)) ([],[])
+
+
+unzip3           :: [(a,b,c)] -> ([a],[b],[c])
+unzip3           =  foldr (\abc o -> case abc of (a,b,c) -> (a:fst3 o,b:snd3 o,c:thd3 o))
+                          ([],[],[])
+
+fst3 x = case x of (x,_,_) -> x
+snd3 x = case x of (_,x,_) -> x
+thd3 x = case x of (_,_,x) -> x
+
+
+type  ReadS a  = String -> [(a,String)]
+
+type  ShowS    = String -> String
+
+
+class  Read a  where
+    readsPrec        :: Int -> ReadS a
+    readList         :: ReadS [a]
+
+
+class  Show a  where
+    showsPrec        :: Int -> a -> ShowS
+    show             :: a -> String 
+    showList         :: [a] -> ShowS
+
+reads            :: (Read a) => ReadS a
+reads            =  readsPrec 0
+
+
+shows            :: (Show a) => a -> ShowS
+shows            =  showsPrec 0
+
+
+showChar         :: Char -> ShowS
+showChar         =  (:)
+
+
+showString       :: String -> ShowS
+showString       =  (++)
+
+
+showParen        :: Bool -> ShowS -> ShowS
+showParen b p    =  if b then showChar '(' . p . showChar ')' else p
+
+
+-- This lexer is not completely faithful to the Haskell lexical syntax.
+-- Current limitations:
+--    Qualified names are not handled properly
+--    Octal and hexidecimal numerics are not recognized as a single token
+--    Comments are not treated properly
+
+
+instance  Show Int  where
+    showsPrec n = showsPrec n . toInteger
+        -- Converting to Integer avoids
+        -- possible difficulty with minInt
+
+
+instance  Read Int  where
+  readsPrec p r = [(fromInteger i, t) | (i,t) <- readsPrec p r]
+        -- Reading at the Integer type avoids
+        -- possible difficulty with minInt
+
+
+instance  Show Integer  where
+    showsPrec           = showSigned showInt
+
+
+instance  Read Integer  where
+    readsPrec p         = readSigned readDec
+
+
+instance  Show Float  where 
+    showsPrec p         = showFloat
+           
+
+instance  Read Float  where
+    readsPrec p         = readSigned readFloat
+
+
+instance  Show Double  where
+    showsPrec p         = showFloat
+
+
+instance  Read Double  where
+    readsPrec p         = readSigned readFloat
+
+
+instance  Show ()  where
+    showsPrec p () = showString "()"
+
+
+instance Read () where
+    readsPrec p    = readParen False
+                            (\r -> [((),t) | ("(",s) <- lex r,
+                                             (")",t) <- lex s ] )
+
+instance  Show Char  where
+    showsPrec p '\'' = showString "'\\''"
+    showsPrec p c    = showChar '\'' . showLitChar c . showChar '\''
+
+    showList cs = showChar '"' . showl cs
+                 where showl ""       = showChar '"'
+                       showl ('"':cs) = showString "\\\"" . showl cs
+                       showl (c:cs)   = showLitChar c . showl cs
+
+
+instance  Read Char  where
+    readsPrec p      = readParen False
+                            (\r -> [(c,t) | ('\'':s,t)<- lex r,
+                                            (c,"\'")  <- readLitChar s])
+
+    readList = readParen False (\r -> [(l,t) | ('"':s, t) <- lex r,
+                                               (l,_)      <- readl s ])
+        where readl ('"':s)      = [("",s)]
+              readl ('\\':'&':s) = readl s
+              readl s            = [(c:cs,u) | (c ,t) <- readLitChar s,
+                                               (cs,u) <- readl t       ]
+
+
+instance  (Show a) => Show [a]  where
+    showsPrec p      = showList
+
+
+instance  (Read a) => Read [a]  where
+    readsPrec p      = readList
+
+-- Tuples
+
+
+instance  (Show a, Show b) => Show (a,b)  where
+    showsPrec p (x,y) = showChar '(' . shows x . showChar ',' .
+                                       shows y . showChar ')'
+
+
+instance  (Read a, Read b) => Read (a,b)  where
+    readsPrec p       = readParen False
+                            (\r -> [((x,y), w) | ("(",s) <- lex r,
+                                                 (x,t)   <- reads s,
+                                                 (",",u) <- lex t,
+                                                 (y,v)   <- reads u,
+                                                 (")",w) <- lex v ] )
+
+-- Other tuples have similar Read and Show instances
+
+type  FilePath = String
+
+
+data IOError    -- The internals of this type are system dependent
+
+
+instance  Show IOError  where
+
+instance  Eq IOError  where
+
+
+ioError    ::  IOError -> IO a 
+ioError    =   primIOError
+   
+
+userError  ::  String -> IOError
+userError  =   primUserError
+   
+
+catch      ::  IO a -> (IOError -> IO a) -> IO a 
+catch      =   primCatch
+   
+
+putChar    :: Char -> IO ()
+putChar    =  primPutChar
+   
+
+putStr     :: String -> IO ()
+putStr s   =  mapM_ putChar s
+   
+
+putStrLn   :: String -> IO ()
+putStrLn s =   putStr s >> putStr "\n"
+   
+
+print      :: Show a => a -> IO ()
+print x    =  putStrLn (show x)
+   
+
+getChar    :: IO Char
+getChar    =  primGetChar
+   
+
+getLine    :: IO String
+getLine    =  getChar >>= \c -> 
+                 if c == '\n' then return "" else 
+                    getLine >>= \s -> 
+                       return (c:s)
+            
+
+getContents :: IO String
+getContents =  primGetContents
+
+
+interact    ::  (String -> String) -> IO ()
+-- The hSetBuffering ensures the expected interactive behaviour
+interact f  =  hSetBuffering stdin  NoBuffering >>
+                  hSetBuffering stdout NoBuffering >>
+                  getContents >>= \s ->
+                  putStr (f s)
+
+
+readFile   :: FilePath -> IO String
+readFile   =  primReadFile
+   
+
+writeFile  :: FilePath -> String -> IO ()
+writeFile  =  primWriteFile
+   
+
+appendFile :: FilePath -> String -> IO ()
+appendFile =  primAppendFile
+
+  -- raises an exception instead of an error
+
+
+readLn :: Read a => IO a
+readLn =   getLine >>= \l ->
+             readIO l >>= \r ->
+             return r
diff --git a/qed.cabal b/qed.cabal
new file mode 100644
--- /dev/null
+++ b/qed.cabal
@@ -0,0 +1,54 @@
+cabal-version:      >= 1.8
+build-type:         Simple
+name:               qed
+version:            0.0
+license:            BSD3
+license-file:       LICENSE
+category:           Theorem Provers
+author:             Neil Mitchell <ndmitchell@gmail.com>
+maintainer:         Neil Mitchell <ndmitchell@gmail.com>
+copyright:          Neil Mitchell 2015
+synopsis:           Simple prover
+description:
+    A prototype proof system.
+homepage:           https://github.com/ndmitchell/qed#readme
+bug-reports:        https://github.com/ndmitchell/qed/issues
+data-files:
+    imports/*.hs
+extra-doc-files:
+    README.md
+    CHANGES.txt
+tested-with:        GHC==7.10.1, GHC==7.8.4
+
+source-repository head
+    type:     git
+    location: https://github.com/ndmitchell/qed.git
+
+library
+    build-depends:
+        base == 4.*, filepath, directory, deepseq,
+        transformers, exceptions,
+        uniplate, extra,
+        haskell-src-exts
+    hs-source-dirs:     src
+    exposed-modules:
+        Proof.QED
+        Proof.QED.Internal
+    other-modules:
+        Paths_qed
+        Proof.Exp.Core
+        Proof.Exp.HSE
+        Proof.Exp.Prop
+        Proof.QED.Trusted
+        Proof.QED.Type
+        Proof.Util
+
+test-suite qed-test
+    type: exitcode-stdio-1.0
+    main-is: Main.hs
+    build-depends: base, qed, transformers
+    hs-source-dirs: test
+
+    other-modules:
+        Classes
+        HLint
diff --git a/src/Proof/Exp/Core.hs b/src/Proof/Exp/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Exp/Core.hs
@@ -0,0 +1,282 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, DeriveDataTypeable, PatternGuards, TupleSections, ViewPatterns #-}
+
+-- | Module for defining and manipulating expressions.
+module Proof.Exp.Core(
+    Var(..), Con(..), Exp(..), Pat(..),
+    fromApps, fromLams, fromLets, lets, lams, apps,
+    isVar,
+    vars, varsP, free, subst, relabel, relabelAvoid, fresh,
+    equivalent,
+    fromExp, fromName,
+    simplifyExp
+    ) where
+
+import Data.Maybe
+import Data.List
+import Data.Data
+import Control.Monad
+import Control.Monad.Trans.State
+import Data.Char
+import Control.Arrow
+import Language.Haskell.Exts hiding (Exp,Name,Pat,Var,Let,App,Case,Con,name,parse,Pretty)
+import qualified Language.Haskell.Exts as H
+import Proof.Exp.HSE
+import Control.DeepSeq
+import Proof.Util hiding (fresh)
+import Data.Generics.Uniplate.Data
+import Control.Applicative
+import Prelude
+
+
+---------------------------------------------------------------------
+-- TYPE
+
+newtype Var = V {fromVar :: String} deriving (Data,Typeable,Eq,Show,Ord,NFData)
+newtype Con = C {fromCon :: String} deriving (Data,Typeable,Eq,Show,Ord,NFData)
+
+data Exp
+    = Var Var
+    | Con Con
+    | App Exp Exp
+    | Let Var Exp Exp -- non-recursive
+    | Lam Var Exp
+    | Case Exp [(Pat,Exp)]
+      deriving (Data,Typeable,Eq,Ord)
+
+data Pat
+    = PCon Con [Var]
+    | PWild
+      deriving (Data,Typeable,Eq,Ord)
+
+instance Read Exp where
+    readsPrec = simpleReadsPrec $ fromExp . deflate . fromParseResult . parseExp
+
+instance Show Exp where
+    show = prettyPrint . unparen . inflate . toExp
+        where unparen (Paren x) = x
+              unparen x = x
+
+
+
+isVar Var{} = True; isVar _ = False
+
+instance NFData Exp where
+    rnf (Var a) = rnf a
+    rnf (Con a) = rnf a
+    rnf (App a b) = rnf2 a b
+    rnf (Let a b c) = rnf3 a b c
+    rnf (Lam a b) = rnf2 a b
+    rnf (Case a b) = rnf2 a b
+
+instance NFData Pat where
+    rnf (PCon a b) = rnf2 a b
+    rnf PWild = ()
+
+caseCon :: Exp -> Maybe ([(Var,Exp)], Exp)
+caseCon o@(Case (fromApps -> (Con c, xs)) alts) = Just $ headNote (error $ "Malformed case: " ++ show o) $ mapMaybe f alts
+    where f (PWild, x) = Just ([], x)
+          f (PCon c2 vs, x) | c /= c2 = Nothing
+                            | length vs /= length xs = error "Malformed arity"
+                            | otherwise = Just (zip vs xs, x)
+caseCon _ = Nothing
+
+apps x (y:ys) = apps (App x y) ys
+apps x [] = x
+
+lams (y:ys) x = Lam y $ lams ys x
+lams [] x = x
+
+lets [] x = x
+lets ((a,b):ys) x = Let a b $ lets ys x
+
+
+fromLets (Let x y z) = ((x,y):a, b)
+    where (a,b) = fromLets z
+fromLets x = ([], x)
+
+fromLams (Lam x y) = (x:a, b)
+    where (a,b) = fromLams y
+fromLams x = ([], x)
+
+fromApps (App x y) = (a,b ++ [y])
+    where (a,b) = fromApps x
+fromApps x = (x,[])
+
+---------------------------------------------------------------------
+-- BINDING AWARE OPERATIONS
+
+vars :: Exp -> [Var]
+vars = universeBi
+
+varsP :: Pat -> [Var]
+varsP = universeBi
+
+free :: Exp -> [Var]
+free (Var x) = [x]
+free (App x y) = nub $ free x ++ free y
+free (Lam x y) = delete x $ free y
+free (Case x y) = nub $ free x ++ concat [free b \\ varsP a | (a,b) <- y]
+free (Let a b y) = nub $ free b ++ delete a (free y)
+free _ = []
+
+
+subst :: [(Var,Exp)] -> Exp -> Exp
+subst [] x = x
+subst ren e = case e of
+    Var x -> fromMaybe (Var x) $ lookup x ren
+    App x y -> App (f [] x) (f [] y)
+    Lam x y -> Lam x (f [x] y)
+    Case x y -> Case (f [] x) [(a, f (varsP a) b) | (a,b) <- y]
+    Let a b y -> Let a (f [] b) $ f [a] y
+    x -> x
+    where f del x = subst (filter (flip notElem del . fst) ren) x
+
+
+relabel :: Exp -> Exp
+relabel x = relabelAvoid (free x) x
+
+relabelAvoid :: [Var] -> Exp -> Exp
+relabelAvoid xs x = evalState (f [] x) (fresh xs)
+    where
+        f :: [(Var,Var)] -> Exp -> State [Var] Exp
+        f mp (Lam v x) = do i <- var; Lam i <$> f ((v,i):mp) x
+        f mp (Let v x y) = do i <- var; Let i <$> f mp x <*> f ((v,i):mp) y
+        f mp (Case x alts) = Case <$> f mp x <*> mapM (g mp) alts
+        f mp (App x y) = App <$> f mp x <*> f mp y
+        f mp (Var x) = return $ Var $ fromMaybe x $ lookup x mp
+        f mp x = return x
+
+        g mp (PWild, x) = (PWild,) <$> f mp x
+        g mp (PCon c vs, x) = do is <- replicateM (length vs) var; (PCon c is,) <$> f (zip vs is ++ mp) x
+
+        var = do s:ss <- get; put ss; return s
+
+fresh :: [Var] -> [Var]
+fresh used = map V (concatMap f [1..]) \\ used
+    where f 1 = map return ['a'..'z']
+          f i = [a ++ b | a <- f 1, b <- f (i-1)]
+
+
+eval :: Exp -> Exp
+eval = relabel . nf . relabel
+    where
+        whnf (Let v x y) = whnf $ subst [(v,x)] y
+        whnf (App (whnf -> Lam v x) y) = whnf $ subst [(v,y)] x
+        whnf (App (whnf -> Case x alts) y) = whnf $ Case x $ map (second $ flip App y) alts
+        whnf (Case (whnf -> x) alts) | Just (bs, bod) <- caseCon $ Case x alts = whnf $ subst bs bod
+        whnf (Case (whnf -> Case x alts1) alts2) = Case x [(a, Case b alts2) | (a,b) <- alts1]
+        whnf x = x
+
+        nf = descend nf . whnf
+
+
+equivalent :: String -> Exp -> Exp -> Exp
+equivalent = equivalentOn eval
+
+
+---------------------------------------------------------------------
+-- SIMPLIFY
+
+simplifyExp :: Exp -> Exp
+simplifyExp = \(relabel -> x) -> equivalent "simplify" x $ idempotent "simplify" fs x
+    where
+        fs = transform f
+
+        f o@(App (fromLets -> (bs@(_:_), Lam v z)) q) = fs $ Let v q $ lets bs z
+        f o@(Case (Let v x y) alts) = fs $ Let v x $ Case y alts
+        {-
+        -- True, but a bit different to the others, since it is information propagation
+        -- Nothing requries it yet
+        f o@(Case (Var v) alts) | map g alts /= alts = fs $ Case (Var v) $ map g alts
+            where g (PCon c vs, x) | v `notElem` vs = (PCon c vs, subst [(v, apps (Con c) $ map Var vs)] x)
+                  g x = x
+        -}
+        f (App (Lam v x) y) = f $ Let v y x
+        f (Let v x y) | cheap x || linear v y = fs $ subst [(v,x)] y
+        f o@(Case (Case on alts1) alts2) =  fs $ Case on $ map g alts1
+            where g (PWild, c) = (PWild, Case c alts2)
+                  g (PCon a vs, c) = (PCon a vs, Case c alts2)
+        f x | Just ((unzip -> (vs, xs)), bod) <- caseCon x = fs $ lets (zip vs xs) bod
+        f x = x
+
+cheap (Var _) = True
+cheap (Con _) = True
+cheap (Lam _ _) = True
+cheap _ = False
+
+
+linear :: Var -> Exp -> Bool
+linear v x = count v x <= 1
+
+count :: Var -> Exp -> Int
+count v (Var x) = if v == x then 1 else 0
+count v (Lam w y) = if v == w then 0 else count v y * 2 -- lambda count is infinite, but 2 is close enough
+count v (Let w x y) = count v x + (if v == w then 0 else count v y)
+count v (Case x alts) = count v x + maximum [if v `elem` varsP p then 0 else count v c | (p,c) <- alts]
+count v (App x y) = count v x + count v y
+count v _ = 0
+
+
+---------------------------------------------------------------------
+-- FROM HSE
+
+fromDecl :: Decl -> [(Var,Exp)]
+fromDecl (PatBind _ (PVar f) (UnGuardedRhs x) (BDecls [])) = [(V $ fromName f, fromExp x)]
+fromDecl TypeSig{} = []
+fromDecl DataDecl{} = []
+fromDecl TypeDecl{} = []
+fromDecl x = error $ "Unhandled fromDecl: " ++ show x
+
+fromExp :: H.Exp -> Exp
+fromExp (Lambda _ [PVar (Ident x)] bod) = Lam (V x) $ fromExp bod
+fromExp (H.App x y) = App (fromExp x) (fromExp y)
+fromExp (H.Var (UnQual x)) = Var $ V $ fromName x
+fromExp (H.Con (UnQual x)) = Con $ C $ fromName x
+fromExp (Paren x) = fromExp x
+fromExp (H.Case x xs) = Case (fromExp x) $ map fromAlt xs
+fromExp (H.Let (BDecls [d]) x) | [(a,b)] <- fromDecl d =  Let a b $ fromExp x
+fromExp x = error $ "Unhandled fromExp: " ++ show x
+
+fromName :: H.Name -> String
+fromName (Ident x) = x
+fromName (Symbol x) = x
+
+fromAlt :: Alt -> (Pat, Exp)
+fromAlt (Alt _ pat (UnGuardedRhs bod) (BDecls [])) = (fromPat pat, fromExp bod)
+fromAlt x = error $ "Unhandled fromAlt: " ++ show x
+
+fromPat :: H.Pat -> Pat
+fromPat (PParen x) = fromPat x
+fromPat (PApp (UnQual c) xs) = PCon (C $ fromName c) $ map (V . fromPatVar) xs
+fromPat PWildCard = PWild
+fromPat x = error $ "Unhandled fromPat: " ++ show x
+
+fromPatVar :: H.Pat -> String
+fromPatVar (PVar x) = fromName x
+fromPatVar x = error $ "Unhandled fromPatVar: " ++ show x
+
+
+---------------------------------------------------------------------
+-- TO HSE
+
+toDecl :: Var -> Exp -> Decl
+toDecl (V f) x = PatBind sl (PVar $ toName f) (UnGuardedRhs $ toExp x) (BDecls [])
+
+toExp :: Exp -> H.Exp
+toExp (Var (V x)) = H.Var $ UnQual $ toName x
+toExp (Con (C x)) = H.Con $ UnQual $ toName x
+toExp (Lam (V x) y) = Lambda sl [PVar $ toName x] $ toExp y
+toExp (Let a b y) = H.Let (BDecls [toDecl a b]) $ toExp y
+toExp (App x y) = H.App (toExp x) (toExp y)
+toExp (Case x y) = H.Case (toExp x) (map toAlt y)
+
+toAlt :: (Pat, Exp) -> Alt
+toAlt (x,y) = Alt sl (toPat x) (UnGuardedRhs $ toExp y) (BDecls [])
+
+toPat :: Pat -> H.Pat
+toPat (PCon (C c) vs) = PApp (UnQual $ toName c) (map (PVar . Ident . fromVar) vs)
+toPat PWild = PWildCard
+
+toName :: String -> H.Name
+toName xs@(x:_) | isAlphaNum x || x `elem` "'_(" = Ident xs
+                | otherwise = Symbol xs
diff --git a/src/Proof/Exp/HSE.hs b/src/Proof/Exp/HSE.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Exp/HSE.hs
@@ -0,0 +1,161 @@
+{-# LANGUAGE ViewPatterns, PatternGuards #-}
+
+-- | Module for operating on haskell-src-exts expressions.
+module Proof.Exp.HSE(deflate, inflate, sl) where
+
+import Data.Data
+import Data.List
+import Language.Haskell.Exts
+import Control.Monad.Trans.State
+import Data.Generics.Uniplate.Data
+import Control.Applicative
+import Prelude
+
+
+-- Turn on to have better list comp desugaring in terms of mapMaybe for common cases
+fasterListComp = False
+
+sl = SrcLoc "" 0 0
+
+names :: Data a => a -> [String]
+names = map f . universeBi
+    where f (Ident x) = x
+          f (Symbol x) = x
+
+fresh :: [String] -> [String]
+fresh del = ["v" ++ show i | i  <- [1..]] \\ del
+
+---------------------------------------------------------------------
+-- DEFLATE
+
+-- | Use fewer constructors to express the same program.
+deflate :: Data a => a -> a
+deflate = transformBi deflateExp . transformBi deflatePat . transformBi deflateQName . transformBi deflateDecl . deflateWildcard
+
+spec :: SpecialCon -> QName
+spec UnitCon = UnQual $ Ident "()"
+spec ListCon = UnQual $ Ident "[]" 
+spec Cons = UnQual $ Symbol ":"
+spec (TupleCon Boxed i) = UnQual $ Ident $ "(" ++ replicate (i-1) ',' ++ ")"
+spec x = Special x
+
+deflateDecl :: Decl -> Decl
+deflateDecl (FunBind [Match sl f vars Nothing (UnGuardedRhs x) decs]) =
+    PatBind sl (PVar f) (UnGuardedRhs $ Lambda sl vars $ Let decs x) (BDecls [])
+deflateDecl x = x
+
+deflateQName :: QName -> QName
+deflateQName (Special x) = spec x
+deflateQName x = x
+
+deflateExp :: Exp -> Exp
+deflateExp (Lambda sl ps x) | length ps /= 1 = foldr (\p x -> Lambda sl [p] x) x ps
+deflateExp (LeftSection x (QVarOp y)) = App (Var y) x
+deflateExp (LeftSection x (QConOp y)) = App (Con y) x
+deflateExp (RightSection (QVarOp y) x) = Paren $ Var (UnQual $ Ident "flip") `App` Var y `App` Paren x
+deflateExp (RightSection (QConOp y) x) = Paren $ Var (UnQual $ Ident "flip") `App` Con y `App` Paren x
+deflateExp (List []) = Con $ spec ListCon
+deflateExp (List (x:xs)) = Paren $ Con (spec Cons) `App` Paren x `App` deflateExp (List xs)
+deflateExp (Tuple b xs) = foldl App (Con $ spec $ TupleCon b $ length xs) xs
+deflateExp (InfixApp a (QVarOp b) c) = Var b `App` a `App` c
+deflateExp (InfixApp a (QConOp b) c) = Con b `App` a `App` c
+deflateExp (Lit x) = Con $ UnQual $ Ident $ prettyPrint x
+deflateExp (NegApp x) = Paren $ Var (UnQual $ Ident "negate") `App` Paren x
+deflateExp o@(Lambda sl [p] e) | not $ isPVar p = Lambda sl [PVar new] $ Case (Var $ UnQual new) [Alt sl p (UnGuardedRhs e) $ BDecls []]
+    where new:_ = map Ident $ fresh $ names o
+deflateExp (Case (Var (UnQual v)) (Alt sl (PVar p) (UnGuardedRhs e) (BDecls []):_))
+    | v == p = e
+    | otherwise = Let (BDecls [PatBind sl (PVar p) (UnGuardedRhs $ Var $ UnQual v) (BDecls [])]) e
+deflateExp (If a b c) = Case a [f "True" b, f "False" c]
+    where f con x = Alt sl (PApp (UnQual $ Ident con) []) (UnGuardedRhs x) (BDecls [])
+deflateExp (Let (BDecls bs) x) = foldr (\b x -> Let (BDecls [b]) x) x bs -- FIXME: Only safe if variables are not mutually recursive
+deflateExp (EnumFromTo x y) = Paren $ Var (UnQual $ Ident "enumFromTo") `App` x `App` y
+deflateExp (EnumFromThen x y) = Paren $ Var (UnQual $ Ident "enumFromThen") `App` x `App` y
+deflateExp (EnumFromThenTo x y z) = Paren $ Var (UnQual $ Ident "enumFromThenTo") `App` x `App` y `App` z
+deflateExp (EnumFrom x) = Paren $ Var (UnQual $ Ident "enumFrom") `App` x
+deflateExp (ListComp res xs) = lst xs
+    where
+        -- variants returning a Maybe
+        may [] = Just $ Con (UnQual $ Ident "Just") `App` Paren res
+        may (QualStmt (LetStmt bind):xs) = deflateExp . Let bind <$> may xs
+        may (QualStmt (Qualifier e):xs) = (\xs -> Paren $ deflateExp $ If e xs $ Con $ UnQual $ Ident "Nothing") <$> may xs
+        may _ = Nothing
+
+        -- optimised shortcuts (use map or mapMaybe)
+        lst (QualStmt (Generator _ p e):[]) | fasterListComp, irrefutable p = Var (UnQual $ Ident "map") `App` deflateExp (Lambda sl [p] res) `App` e
+        lst o@(QualStmt (Generator _ p e):xs) | fasterListComp, Just ans <- may xs =
+            Var (UnQual $ Ident "mapMaybe") `App` deflateExp (Lambda sl [PVar new] $ bod ans) `App` e
+            where new:_ = map Ident $ fresh $ names $ ListComp res o
+                  bod ans = deflateExp $ Case (Var $ UnQual new) $
+                            [Alt sl p (UnGuardedRhs ans) $ BDecls []] ++
+                            [Alt sl PWildCard (UnGuardedRhs $ Con $ UnQual $ Ident "Nothing") $ BDecls [] | not $ irrefutable p]
+
+        -- from the report, returning a list
+        lst o@(QualStmt (Generator _ p e):xs) = Var (UnQual $ Ident "concatMap") `App` deflateExp (Lambda sl [PVar new] bod) `App` e
+          where new:_ = map Ident $ fresh $ names $ ListComp res o
+                bod = deflateExp $ Case (Var $ UnQual new)
+                          [Alt sl p (UnGuardedRhs $ lst xs) $ BDecls []
+                          ,Alt sl PWildCard (UnGuardedRhs $ deflateExp $ List []) $ BDecls []]
+        lst (QualStmt (Qualifier e):xs) = Paren $ deflateExp $ If e (lst xs) (deflateExp $ List [])
+        lst (QualStmt (LetStmt bind):xs) = Paren $ deflateExp $ Let bind $ lst xs
+        lst [] = deflateExp $ List [res]
+        lst xs = ListComp res xs
+deflateExp x = x
+
+irrefutable :: Pat -> Bool
+irrefutable x = case deflatePat x of
+    PApp (UnQual (Ident ('(':(dropWhile (== ',') -> ")")))) xs -> all irrefutable xs
+    PVar{} -> True
+    _ -> False
+
+deflatePat :: Pat -> Pat
+deflatePat (PInfixApp a b c) = PApp b [a,c]
+deflatePat (PList []) = PApp (spec ListCon) []
+deflatePat (PTuple b xs) = PApp (spec $ TupleCon b $ length xs) xs
+deflatePat x = x
+
+-- removing wildcards needs some state (the unused variables), so has to be monadic
+deflateWildcard :: Data a => a -> a
+deflateWildcard x = evalState (transformBiM f x) (["_" ++ show i | i <- [1..]] \\ names x)
+    where f :: Pat -> State [String] Pat
+          f PWildCard = do s:ss <- get; put ss; return $ PVar $ Ident s
+          f x = return x
+
+isPVar PVar{} = True; isPVar _ = False
+
+
+---------------------------------------------------------------------
+-- INFLATE
+
+-- | Add back in syntactic forms to make it more readable.
+inflate :: Data a => a -> a
+inflate =
+    transformBi inflateRhs . transformBi inflateAlt . transformBi inflateRhs .
+    transformBi inflatePat . transformBi inflateExp .
+    transformBi Paren . transformBi PParen
+
+inflateExp :: Exp -> Exp
+inflateExp (Lambda sl ps (Paren x)) = inflateExp $ Lambda sl ps x
+inflateExp (Lambda sl ps1 (Lambda _ ps2 x)) | null $ names ps1 `intersect` names ps2 = Lambda sl (ps1++ps2) x
+inflateExp (Paren (Paren x)) = inflateExp $ Paren x
+inflateExp (Paren (Var x)) = Var x
+inflateExp (Paren (Con x)) = Con x
+inflateExp (Paren (List x)) = List x
+inflateExp (Paren (Lit x)) = Lit x
+inflateExp (App (Paren (App a b)) c) = App (App a b) c
+inflateExp (Con (UnQual (Symbol "[]"))) = List []
+inflateExp x = x
+
+inflatePat :: Pat -> Pat
+inflatePat (PParen (PParen x)) = PParen x
+inflatePat (PParen (PVar x)) = PVar x
+inflatePat (PApp (UnQual (Symbol "[]")) []) = PList []
+inflatePat x = x
+
+inflateRhs :: Rhs -> Rhs
+inflateRhs (UnGuardedRhs (Paren x)) = UnGuardedRhs x
+inflateRhs x = x
+
+inflateAlt :: Alt -> Alt
+inflateAlt (Alt sl (PParen p) x y) = Alt sl p x y
+inflateAlt x = x
diff --git a/src/Proof/Exp/Prop.hs b/src/Proof/Exp/Prop.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Exp/Prop.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE DeriveDataTypeable, PatternGuards, TupleSections, ViewPatterns #-}
+
+-- | Module for defining and manipulating expressions.
+module Proof.Exp.Prop(
+    Prop(..), sym, tautology, simplifyProp, (==>)
+    ) where
+
+import Proof.Exp.Core
+import Proof.Util
+import Data.Data
+import Data.Maybe
+import Data.List.Extra
+import Control.DeepSeq
+
+data Prop = Prop [Var] Exp Exp deriving (Eq,Data,Typeable)
+
+instance NFData Prop where
+    rnf (Prop a b c) = rnf3 a b c
+
+sym :: Prop -> Prop
+sym (Prop vs a b) = Prop vs b a
+
+instance Show Prop where
+    show (Prop vs a b) = unwords (map fromVar vs ++ ["=>"]) ++ "\n" ++ f a ++ "=" ++ drop 1 (f b)
+        where f = unlines . map ("  "++) . lines . show
+
+instance Read Prop where
+    readsPrec = simpleReadsPrec $ \x -> case () of
+        _ | (quant, x) <- fromMaybe ("",x) $ stripInfix " => " x
+          , Just (a,b) <- stripInfix " = " x
+          -> Prop (map V $ words quant) (read a) (read b)
+
+simplifyProp :: Prop -> Prop
+simplifyProp = label . simple . unlam . simple
+    where
+        simple (Prop vs a b) = Prop vs (simplifyExp a) (simplifyExp b)
+
+        unlam (Prop vs (Lam a1 a2) (Lam b1 b2))
+            | v:_ <- fresh $ a1:b1:vs ++ vars a2 ++ vars b2
+            = unlam $ Prop (v:vs) (subst [(a1,Var v)] a2) (subst [(b1,Var v)] b2)
+        unlam x = x
+
+        label (Prop vs a b) = Prop new (subst sub $ relabelAvoid (free a ++ new) a) (subst sub $ relabelAvoid (free b ++ new) b)
+            where fv = nubOrd $ free a ++ free b
+                  vs2 = fv `intersect` vs
+                  new = take (length vs2) $ fresh $ fv \\ vs
+                  sub = zip vs2 $ map Var new
+
+
+-- Does the first property imply the second
+(==>) :: Prop -> Prop -> Bool
+(==>) a b = simplifyProp a == simplifyProp b || simplifyProp (sym a) == simplifyProp b
+
+tautology :: Prop -> Bool
+tautology (Prop vs a b) = a == b
diff --git a/src/Proof/QED.hs b/src/Proof/QED.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/QED.hs
@@ -0,0 +1,461 @@
+{-# LANGUAGE ViewPatterns, ScopedTypeVariables, RecordWildCards, TupleSections, PatternGuards #-}
+
+module Proof.QED(
+    QED, qed,
+    imports, decl,
+    Laws, law, laws,
+    Proof, PropString, prove,
+    Bind, satisfy, bind,
+    rhs, lhs, bhs, at,
+    recurse, unfold, unfold_, strict, expand, unlet, divide,
+    twice, thrice, many, perhaps, skip,
+    qedCheat, unsafeCheat
+    ) where
+
+import Proof.QED.Internal() -- so I test all the API's
+
+import Proof.QED.Type
+import Proof.QED.Trusted
+import Proof.Exp.Prop
+import Proof.Exp.Core
+import Proof.Exp.HSE
+import Control.Monad.IO.Class
+import Control.Monad.Catch as C
+import Control.Monad
+import Language.Haskell.Exts hiding (Var, Exp, Con, Case, App, Let)
+import Data.Maybe
+import Data.List.Extra
+import System.FilePath
+import System.Directory
+import Data.Generics.Uniplate.Data
+import Paths_qed
+import Control.Applicative hiding (many)
+import Prelude
+
+type PropString = String
+
+law :: PropString -> QED Laws
+law (read -> p) = do
+    addAssumed p
+    return $ Laws [p]
+
+laws :: QED a -> QED Laws
+laws act = do
+    n <- length . assumed <$> getKnown
+    act
+    Laws . drop n . assumed <$> getKnown
+
+imports :: FilePath -> QED ()
+imports file = do
+    dataDir <- liftIO getDataDir
+    let poss = [dir </> file <.> ext | dir <- [".",dataDir </> "imports"], ext <- [".hs",""]]
+    files <- liftIO $ filterM doesFileExist poss
+    when (null files) $
+        fail $ unlines $ ("imports: Could not find " ++ file ++ ", tried:") : map ("  "++) poss
+    src <- liftIO $ readFile $ head files
+    let mode = defaultParseMode{parseFilename=file}
+    let res = deflate $ fromParseResult $ parseFileContentsWithMode mode $ replace "..." "undefined" src
+    mapM_ addDecl $ childrenBi res
+
+decl :: String -> QED ()
+decl = addDecl . deflate . fromParseResult . parseDecl
+
+addDecl :: Decl -> QED ()
+addDecl (PatBind _ (PVar name) (UnGuardedRhs bod) (BDecls [])) = addDefinition (V $ fromName name) (fromExp bod)
+addDecl (DataDecl _ _ _ name _ ctrs _) = addType (fromName name) [(C $ fromName a, length b) | (QualConDecl _ _ _ (ConDecl a b)) <- ctrs]
+addDecl x@ClassDecl{} = mapM_ addDecl $ children x
+addDecl InfixDecl{} = return ()
+addDecl InstDecl{} = return ()
+addDecl TypeDecl{} = return ()
+addDecl TypeSig{} = return ()
+addDecl x = error $ "Cannot add declaration, " ++ prettyPrint x
+
+
+prove :: PropString -> Proof () -> QED ()
+prove (read -> prop) proof = addProved prop proof
+
+satisfy :: String -> Laws -> Bind () -> QED ()
+satisfy msg (Laws ps) (runBind -> bind) = do
+    liftIO $ putStrLn $ "Satisfy " ++ msg
+    Known{..} <- getKnown
+    forM_ ps $ \(Prop vs a b) -> do
+        let p2 = Prop vs (subst bind a) (subst bind b)
+        unless (any (==> p2) (assumed ++ proved)) $ do
+            fail $ "Failed to satisfy:" ++ show p2
+    liftIO $ putStrLn "QED\n"
+
+unfold :: String -> Proof ()
+unfold name = apply rewriteUnfold $ \Known{..} x -> case x of
+    Var x | x == V name, Just e <- lookup x definitions -> Just e
+    _ -> Nothing
+
+unfold_ :: Proof ()
+unfold_ = apply rewriteUnfold $ \Known{..} x -> case x of
+    Var x | Just e <- lookup x definitions -> Just e
+    _ -> Nothing
+
+strict :: String -> Proof ()
+strict name = apply rewriteEquivalent $ \Known{..} x -> case x of
+    Var x -> Just $ Case (Var x)
+        [ (PCon c vars, apps (Con c) $ map Var vars)
+        | (c,vs) <- fromJust $ lookup name types, let vars = take vs $ fresh []]
+    _ -> Nothing
+
+recurse :: Proof ()
+recurse = rewriteRecurse >> auto
+
+expand :: Proof ()
+expand = apply rewriteEquivalent $ \Known{..} o@(fromLams -> (vs, x)) -> Just $
+    let v:_ = fresh $ vars o 
+    in lams (vs ++ [v]) $ App x $ Var v
+
+
+unlet :: Proof ()
+unlet = apply rewriteEquivalent $ \_ x ->
+    case x of Let a b x -> Just $ subst [(a,b)] x; _ -> Nothing
+
+divide :: Proof ()
+divide = do
+    rewriteSplit
+    auto
+
+
+twice :: Proof () -> Proof ()
+twice = replicateM_ 2
+
+thrice :: Proof () -> Proof ()
+thrice = replicateM_ 3
+
+many :: Proof () -> Proof ()
+many p = void $ p >> perhaps (forever p)
+
+rhs :: Proof () -> Proof ()
+rhs = side RHS
+
+lhs :: Proof () -> Proof ()
+lhs = side LHS
+
+side :: Side -> Proof () -> Proof ()
+side x act = C.bracket
+    (focusSide . snd <$> getUnknown)
+    setFocusSide $
+    const $ setFocusSide (Just x) >> act
+
+bhs :: Proof () -> Proof ()
+bhs p = lhs p >> rhs p
+
+at :: Int -> Proof () -> Proof ()
+at i act = C.bracket
+    (focusAt . snd <$> getUnknown)
+    setFocusAt $
+    const $ setFocusAt i >> act
+
+bind :: String -> Bind ()
+bind (deflate . fromParseResult . parseDecl -> PatBind _ (PVar name) (UnGuardedRhs bod) (BDecls [])) =
+    addBind (V $ fromName name) (fromExp bod)
+
+
+apply :: (Prop -> Proof ()) -> (Known -> Exp -> Maybe Exp) -> Proof ()
+apply run test = do
+    (known, Unknown{..}, Goal pre (Prop vs lhs rhs)) <- getGoal
+    let poss = (if focusSide /= Just RHS then map (,\lhs -> Prop vs lhs rhs) $ contexts lhs else []) ++
+               (if focusSide /= Just LHS then map (,\rhs -> Prop vs lhs rhs) $ contexts rhs else [])
+    let xs = [gen2 $ gen x | ((test known -> Just x, gen),gen2) <- poss]
+    case drop focusAt xs of
+        [] -> badProof "Cannot apply, no suitable elements at index"
+        x:_ -> run x >> auto
+
+auto :: Proof ()
+auto = f autos
+    where
+        autos = [rewriteTautology, autoSimplify, autoPeel]
+
+        f [] = return ()
+        f (a:as) = do
+            r <- perhaps a
+            f $ if r then autos else as
+
+
+autoSimplify :: Proof ()
+autoSimplify = do
+    (_, _, Goal _ x) <- getGoal
+    let x2 = simplifyProp x
+    if x2 == x then badProof "cannot autoSimplify" else rewriteEquivalent x2
+
+autoPeel :: Proof ()
+autoPeel = do
+    (_, _, Goal _ (Prop vs a b)) <- getGoal
+    if f vs a && f vs b then rewriteSplit else badProof "cannot autoPeel"
+    where
+        f vs Lam{} = True
+        f vs Con{} = True
+        f vs (App x _) = f vs x
+        f vs (Var v) = v `elem` vs
+        f vs (Case (Var v) _) = v `elem` vs
+        f vs _ = False
+
+
+perhaps :: Proof () -> Proof Bool
+perhaps x = not <$> isBadProof x
+
+skip :: QED () -> QED ()
+skip _ = return ()
+
+{-
+autoLaw :: State -> Goal -> Maybe [Goal]
+autoLaw s (Goal pre x)
+    | tautology x = Just []
+    | any (==> x) (pre ++ proved s) = Just []
+    | otherwise = Nothing
+
+autoPeelCase :: Goal -> Maybe [Goal]
+autoPeelCase (Goal pre (Prop vs a b))
+    | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)
+    | otherwise = Nothing
+    where
+        -- distinguishes the salient features
+        pattern (Case on alts) = Just (on, map (patCon . fst) alts)
+        pattern x = Nothing
+
+        split (Case on alts) = [lams (patVars p) $ f on p x | (p,x) <- alts]
+            where f (Var on) (PCon c vs) | on `notElem` vs = Let on (apps (Con c) (map Var vs))
+                  f _ _ = id
+
+autoPeelCon :: Goal -> Maybe [Goal]
+autoPeelCon (Goal pre (Prop vs a b))
+    | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)
+    | otherwise = Nothing
+    where
+        pattern (fromApps -> (Con ctr, args)) = Just (ctr, length args)
+        pattern x = Nothing
+
+        split (fromApps -> (Con ctr, args)) = map (lams vs) args
+
+autoPeelVar :: Goal -> Maybe [Goal]
+autoPeelVar (Goal pre (Prop vs a b))
+    | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)
+    | otherwise = Nothing
+    where
+        pattern (fromApps -> (Var v, args)) | v `elem` vs = Just (v, length args)
+        pattern x = Nothing
+
+        split (fromApps -> (Var v, args)) = args
+-}
+
+
+{-
+
+data State = State
+    {defined :: [(Var, Exp)]
+    ,types :: [(String, [(Con,Int)])]
+    ,proved :: [Prop]
+    ,goal :: [Goal] -- A list of And alternatives
+    ,focusRhs :: Bool
+    ,focusInd :: Int
+    } deriving Show
+
+instance NFData State where
+    rnf x = rnf $ show x
+
+instance Pretty State where
+    pretty State{..} = unlines $
+        [unwords $ "data" : x : "=" : intercalate ["|"] [fromCon y : replicate n "_" | (y,n) <- ys] | (x,ys) <- types] ++
+        ["\n" ++ fromVar x ++ " = " ++ pretty b | (x,b) <- defined] ++
+        ["\n" ++ pretty x | x <- proved] ++
+        ["\n-- GOAL " ++ show i ++ concat ["\n-- WHERE " ++ pretty p | p <- pre] ++ "\n" ++ pretty x | (i,Goal pre x) <- zip [1..] goal]
+
+state0 = State [] [] [] [] False 0
+
+data Goal = Goal [Prop] Prop deriving (Show,Eq)
+
+state :: IORef State
+state = unsafePerformIO $ newIORef $ state0
+
+getState :: IO State
+getState = readIORef state
+
+modifyState :: (State -> State) -> IO ()
+modifyState f = do
+    s <- readIORef state
+    let s2 = f s
+    evaluate $ rnf s2
+    writeIORef state s2
+
+rhs :: IO a -> IO a
+rhs f = bracket getState
+    (\v -> modifyState $ \s -> s{focusRhs=focusRhs v})
+    (\_ -> do modifyState $ \s -> s{focusRhs=True}; f)
+
+ind :: Int -> IO a -> IO a
+ind i f = bracket getState
+    (\v -> modifyState $ \s -> s{focusInd=focusInd v})
+    (\_ -> do modifyState $ \s -> s{focusInd=i}; f)
+
+run :: IO a -> IO ()
+run act = flip onException dump $ do
+    writeIORef state state0
+    act
+    -- dump
+    g <- goal <$> getState
+    when (null g) $ putStrLn "QED"
+
+dump :: IO ()
+dump = do
+    x <- getState
+    putStrLn $ pretty x
+
+cheat :: IO ()
+cheat = modifyState $ \s -> s{goal = []}
+
+define :: String -> IO ()
+define x = case deflate $ fromParseResult $ parseDecl x of
+    DataDecl _ _ _ name _ ctrs _ -> do
+        let f (fromName -> x) = fromMaybe x $ lookup x [("Nil_","[]"),("Cons_",":")]
+        modifyState $ \s -> s{types = types s ++ [(f name, [(C $ f a,length b) | (QualConDecl _ _ _ (ConDecl a b)) <- ctrs])]}
+    PatBind _ (PVar x) (UnGuardedRhs bod) (BDecls []) -> do
+        let res = fromExp bod
+        evaluate $ show res
+        modifyState $ \s -> s{defined = defined s ++ [(V $ fromName x, res)]}
+    x -> error $ "Define not handled, " ++ show x
+
+proof :: String -> String -> IO () -> IO (IO ())
+proof (parse -> a) (parse -> b) = proofProp (Prop [] a b)
+
+proofProp :: Prop -> IO () -> IO (IO ())
+proofProp p c = do
+    g <- goal <$> getState
+    unless (null g) $ error "Can't call proof recursively"
+    p <- return $ simplifyProp p
+    modifyState $ \s -> s{goal = auto s $ Goal [] p}
+    c
+    g <- goal <$> getState
+    unless (null g) $ error "proof did not prove the goal"
+    modifyState $ \s -> s{proved = proved s ++ [p]}
+    return c
+
+
+step :: String -> (State -> Exp -> Maybe Exp) -> IO ()
+step msg f = modifyState $ \s ->
+    let ff = f s
+        Goal pre g1:gs = goal s
+        swp = if focusRhs s then sym else id
+        g2 = (!! focusInd s) $
+             [swp $ gen e | (e, gen) <- contextsBi $ swp g1, Just e <- [ff e]] ++
+             error ("nothing matches, " ++ msg)
+    in s{goal = auto s (Goal pre g2) ++ gs}
+
+expand :: IO ()
+expand = step "Eta expand" $ \_ o@(fromLams -> (vs,x)) -> Just $
+    let v:_ = fresh $ vars o 
+    in lams (vs ++ [v]) $ App x $ Var v
+
+unfold :: String -> IO ()
+unfold x = step ("unfold " ++ x) $ \s ->
+    let rep =
+            case () of
+                _ | Just e <- lookup (V x) $ defined s -> \v -> if v == x then Just e else Nothing
+                  | Just e <- lookup x $ types s -> \v -> Just $ Case (Var (V v))
+                      [(PCon c vs, apps (Con c) (map Var vs)) | (c, n) <- e, let vs = take n $ fresh []]
+                  | otherwise -> error $ "Unknown unfolding for " ++ x
+    in \x -> case x of Var (V v) -> rep v; _ -> Nothing
+
+unlet :: IO ()
+unlet = step "unlet" $ \_ x ->
+    case x of Let a b x -> Just $ subst [(a,b)] x; _ -> Nothing
+
+unsafeReplace :: String -> String -> IO ()
+unsafeReplace (parse -> a) (parse -> b) = step "replace" $ \_ x ->
+    if x == a then Just b else Nothing
+
+auto :: State -> Goal -> [Goal]
+auto s = f full
+    where
+        full = [autoSimplify, autoLaw s, autoPeelCase, autoPeelCon, autoPeelVar]
+
+        f [] g = [g]
+        f (x:xs) g = case x g of
+            Nothing -> f xs g
+            Just [g2] | g == g2 -> f xs g
+            Just gs -> concatMap (f full) gs
+
+
+autoSimplify :: Goal -> Maybe [Goal]
+autoSimplify (Goal pre x) = Just [Goal pre $ simplifyProp x]
+
+autoLaw :: State -> Goal -> Maybe [Goal]
+autoLaw s (Goal pre x)
+    | tautology x = Just []
+    | any (==> x) (pre ++ proved s) = Just []
+    | otherwise = Nothing
+
+autoPeelCase :: Goal -> Maybe [Goal]
+autoPeelCase (Goal pre (Prop vs a b))
+    | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)
+    | otherwise = Nothing
+    where
+        -- distinguishes the salient features
+        pattern (Case on alts) = Just (on, map (patCon . fst) alts)
+        pattern x = Nothing
+
+        split (Case on alts) = [lams (patVars p) $ f on p x | (p,x) <- alts]
+            where f (Var on) (PCon c vs) | on `notElem` vs = Let on (apps (Con c) (map Var vs))
+                  f _ _ = id
+
+autoPeelCon :: Goal -> Maybe [Goal]
+autoPeelCon (Goal pre (Prop vs a b))
+    | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)
+    | otherwise = Nothing
+    where
+        pattern (fromApps -> (Con ctr, args)) = Just (ctr, length args)
+        pattern x = Nothing
+
+        split (fromApps -> (Con ctr, args)) = map (lams vs) args
+
+autoPeelVar :: Goal -> Maybe [Goal]
+autoPeelVar (Goal pre (Prop vs a b))
+    | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)
+    | otherwise = Nothing
+    where
+        pattern (fromApps -> (Var v, args)) | v `elem` vs = Just (v, length args)
+        pattern x = Nothing
+
+        split (fromApps -> (Var v, args)) = args
+
+{-
+
+autoRemoveLam :: IO ()
+autoRemoveLam = modifyState $ \s -> s{goal = [Goal pre $ f x | Goal pre x <- goal s]}
+    where
+        f (a :=: b) | unused <- pattern a `intersect` pattern b = split unused a :=: split unused b
+
+        pattern (fromLams -> (vs, x)) = [i | (i,v) <- zip [0..] vs, v `notElem` free x]
+        split unused (fromLams -> (vs, x)) = lams [v | (i,v) <- zip [0..] vs, i `notElem` unused] x
+-}
+
+recurse :: IO ()
+recurse = modifyState $ \s ->
+    let Goal pre p@(Prop vs a b):gs = goal s
+    in case (reduce s a, reduce s b) of
+        (Nothing, Nothing) -> error $ "Cannot reduce\n" ++ pretty a ++ "\n" ++ pretty b
+        (aa, bb) -> s{goal = auto s (Goal (p:pre) $ Prop vs (fromMaybe a aa) (fromMaybe b bb)) ++ gs}
+
+reduce :: State -> Exp -> Maybe Exp
+reduce State{..} = f
+    where
+        f (Lam v x) = Lam v <$> f x
+        f (App a b) = (`App` b) <$> f a
+        f (Var v) = lookup v defined
+        f (Case x xs) = (`Case` xs) <$> f x
+        f x = error $ "step: Don't know, " ++ pretty x
+
+divide :: IO ()
+divide = modifyState $ \s ->
+    let Goal pre (Prop vs a b):gs = goal s in
+    case (f a, f b) of
+        (Just (oa, ca), Just (ob, cb)) | oa == ob, length ca == length cb ->
+            s{goal = concat (zipWith (\a b -> auto s $ Goal pre $ Prop vs a b) ca cb) ++ gs}
+    where
+        z = Var $ V ""
+        f (App a b) = Just (App z z, [a,b])
+        f _ = Nothing
+-}
diff --git a/src/Proof/QED/Internal.hs b/src/Proof/QED/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/QED/Internal.hs
@@ -0,0 +1,17 @@
+
+module Proof.QED.Internal(
+    Exp(..), Pat(..), Var(..), Con(..),
+    Prop(..),
+    Side(..),
+    Known(..), getKnown,
+    Unknown(..), getUnknown,
+    Goal(..), getGoal,
+    BadProof(..), badProof, isBadProof,
+    Laws(..),
+    module Proof.QED.Trusted
+    ) where
+
+import Proof.Exp.Core
+import Proof.Exp.Prop
+import Proof.QED.Type
+import Proof.QED.Trusted
diff --git a/src/Proof/QED/Trusted.hs b/src/Proof/QED/Trusted.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/QED/Trusted.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE RecordWildCards, PatternGuards #-}
+
+module Proof.QED.Trusted(
+    rewriteUnfold,
+    rewriteEquivalent,
+    rewriteRecurse,
+    rewriteSplit,
+    rewriteTautology
+    ) where
+
+import Proof.Exp.Prop
+import Proof.Exp.Core
+import Proof.QED.Type
+import Control.Monad
+import Data.Maybe
+import Data.Generics.Uniplate.Data
+import Control.Applicative
+import Prelude
+
+
+-- | Use a new prop which is the same as the previous goal, but with any number of unfoldings
+rewriteUnfold :: Prop -> Proof ()
+rewriteUnfold new@(Prop nv na nb) = do
+    (Known{..}, _, Goal ps (Prop ov oa ob)) <- getGoal
+    checkEqual nv ov
+    checkUnfold definitions ov oa na
+    checkUnfold definitions ov ob nb
+    unsafeReplaceFirstGoal [Goal ps new]
+
+checkEqual a b = when (a /= b) $ badProof $ "Not equal, " ++ show a ++ " vs " ++ show b
+
+checkUnfold defs vars old new = unless (f old new) $ badProof $ "Trusted, invalid unfolding"
+    where
+        -- variables that have been captured, err on being too conservative
+        vars2 = vars ++ concat [childrenBi $ descend (const $ Con $ C "") x | x <- universe old, not $ isVar x]
+
+        f (Var v) e | e /= Var v, v `notElem` vars2, Just x <- lookup v defs = e == x
+        f x y = descend (const $ Var $ V "") x == descend (const $ Var $ V "") y &&
+                and (zipWith f (children x) (children y))
+
+
+-- | Use a new prop which is the same as the first goals prop, but with simplified/rearranged expressions
+rewriteEquivalent :: Prop -> Proof ()
+rewriteEquivalent new@(Prop nv na nb) = do
+    (_, _, Goal pre (Prop ov oa ob)) <- getGoal
+    unsafeReplaceFirstGoal [Goal pre new]
+
+
+-- | Apply the coinduction principle on the computation
+rewriteRecurse :: Proof ()
+rewriteRecurse = do
+    (known, _, Goal pre p@(Prop vs a b)) <- getGoal
+    case (reduce known a, reduce known b) of
+        (Nothing, Nothing) -> badProof $ "Cannot reduce\n" ++ show a ++ "\n" ++ show b
+        (aa, bb) -> unsafeReplaceFirstGoal [Goal (p:pre) $ Prop vs (fromMaybe a aa) (fromMaybe b bb)]
+
+reduce :: Known -> Exp -> Maybe Exp
+reduce Known{..} = f
+    where
+        f (Lam v x) = Lam v <$> f x
+        f (App a b) = (`App` b) <$> f a
+        f (Var v) = lookup v definitions
+        f (Case x xs) = (`Case` xs) <$> f x
+        f x = error $ "step: Don't know, " ++ show x
+
+
+-- | Split the expression into multiple subexpressions
+rewriteSplit :: Proof ()
+rewriteSplit = do
+    (_, _, Goal pre (Prop vs a b)) <- getGoal
+    checkEqual (descend (const $ Con $ C "") a) (descend (const $ Con $ C "") b)
+    when (null $ children a) $ badProof "No children to split apart"
+    case (a,b) of
+        (Lam v a, Lam _ b) | v `notElem` vs -> unsafeReplaceFirstGoal [Goal pre $ Prop (vs ++ [v]) a b]
+        _ -> unsafeReplaceFirstGoal $ zipWith (\a b -> Goal pre $ Prop vs a b) (f a) (f b)
+    where
+        f (App a b) = [a,b]
+        f (Case a bs) = a : map g bs
+            where g (PCon c vs, e) = lams vs e
+        f (Let _ a b) = [a,b]
+
+
+-- | The first goal is a tautology
+rewriteTautology :: Proof ()
+rewriteTautology = do
+    (Known{..}, _, Goal pre p) <- getGoal
+    if tautology p || any (==> p) (pre ++ proved) then
+        unsafeReplaceFirstGoal []
+     else
+        badProof "Not a tautology"
diff --git a/src/Proof/QED/Type.hs b/src/Proof/QED/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/QED/Type.hs
@@ -0,0 +1,175 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, DeriveDataTypeable, BangPatterns, TupleSections, PatternGuards #-}
+
+module Proof.QED.Type(
+    Known(..), Unknown(..), Goal(..), Side(..),
+    QED, getKnown, qed, qedCheat,
+    addDefinition, addType, addAssumed, addProved,
+    Proof, getUnknown, getGoal, setFocusSide, setFocusAt,
+    BadProof(..), badProof, isBadProof,
+    unsafeReplaceFirstGoal, unsafeCheat,
+    Bind, addBind, runBind,
+    Laws(..),
+    ) where
+
+import Control.Monad.Trans.State
+import Control.Monad.Trans.Reader
+import Control.Monad.Trans.Writer
+import Control.Monad.Catch as C
+import Control.Monad.IO.Class
+import Control.Exception
+import Control.DeepSeq
+import Control.Monad
+import Data.IORef
+import Data.Typeable
+import Proof.Util
+import Proof.Exp.Core
+import Proof.Exp.Prop
+import Control.Applicative
+import Data.Monoid
+import Prelude
+
+newtype Laws = Laws [Prop]
+    deriving Monoid
+
+
+---------------------------------------------------------------------
+-- KNOWN STATE
+
+newtype QED a = QED (StateT Known IO a)
+    deriving (Functor, Applicative, Monad, MonadIO)
+
+qed :: QED a -> IO ()
+qed (QED x) = void $ execStateT x (Known [] builtinTypes [] [] False)
+
+qedCheat :: QED a -> IO ()
+qedCheat act = qed $ do
+    modifyKnown $ \s -> s{cheater=True}
+    act
+
+builtinTypes :: [(String,[(Con,Int)])]
+builtinTypes =
+    [("[]",[(C "[]",0),(C ":",2)])]
+
+-- | All these things are append only
+data Known = Known
+    {definitions :: [(Var, Exp)]
+    ,types :: [(String, [(Con,Int)])]
+    ,assumed :: [Prop]
+    ,proved :: [Prop]
+    ,cheater :: Bool
+    } deriving Show
+
+instance NFData Known where
+    rnf (Known a b c d e) = rnf5 a b c d e
+
+getKnown :: QED Known
+getKnown = QED get
+
+modifyKnown :: (Known -> Known) -> QED ()
+modifyKnown f = QED $ do
+    x <- get
+    x <- return $ f x
+    liftIO $ evaluate $ rnf x
+    put x
+
+addDefinition :: Var -> Exp -> QED ()
+addDefinition a b = modifyKnown $ \s -> s{definitions = definitions s ++ [(a,b)]}
+
+addType :: String -> [(Con,Int)] -> QED ()
+addType a b = modifyKnown $ \s -> s{types = types s ++ [(a,b)]}
+
+addAssumed :: Prop -> QED ()
+addAssumed a = modifyKnown $ \s -> s{assumed = assumed s ++ [a]}
+
+addProved :: Prop -> Proof () -> QED ()
+addProved prop proof = do
+    liftIO $ putStr $ show prop
+    unknown <- liftIO $ newIORef $ Unknown [Goal [] prop] Nothing 0
+    Proof proof <- return $ do
+        proof
+        unknown <- getUnknown
+        unless (null $ goals $ snd unknown) $ do
+            badProof $ "Did not prove goals"
+    known <- QED get
+    liftIO $ proof `runReaderT` (known, unknown) `C.onException` do
+        print . goals =<< readIORef unknown
+    modifyKnown $ \s -> s{proved = proved s ++ [prop]}
+    liftIO $ putStrLn "QED\n"
+
+
+---------------------------------------------------------------------
+-- UNKNOWN STATE
+
+data Unknown = Unknown
+    {goals :: [Goal] -- A list of And alternatives
+    ,focusSide :: Maybe Side
+    ,focusAt :: Int
+    } deriving Show
+
+data Side = LHS | RHS deriving (Show,Eq)
+
+data Goal = Goal [Prop] Prop deriving Show
+
+instance NFData Unknown where
+    rnf (Unknown a b c) = rnf3 a b c
+
+instance NFData Side where
+    rnf LHS = ()
+    rnf RHS = ()
+
+instance NFData Goal where
+    rnf (Goal a b) = rnf2 a b
+
+newtype Proof a = Proof (ReaderT (Known, IORef Unknown) IO a)
+    deriving (Functor, Applicative, Monad, MonadIO, MonadThrow, MonadCatch, MonadMask)
+
+getUnknown :: Proof (Known, Unknown)
+getUnknown = Proof $ do (k,u) <- ask; liftIO $ (k,) <$> readIORef u
+
+getGoal :: Proof (Known, Unknown, Goal)
+getGoal = do
+    (known, unknown) <- getUnknown
+    case goals unknown of
+        [] -> badProof "No goals left, proof is already complete"
+        g:gs -> return (known, unknown, g)
+
+unsafeReplaceFirstGoal :: [Goal] -> Proof ()
+unsafeReplaceFirstGoal x = do
+    liftIO $ evaluate $ rnf x
+    (_, u) <- Proof ask
+    liftIO $ modifyIORef u $ \s -> s{goals = x ++ drop 1 (goals s)}
+
+unsafeCheat :: String -> Proof ()
+unsafeCheat msg = do
+    (known, _) <- getUnknown
+    unless (cheater known) $ badProof "Must use qedCheat to enable cheating"
+    unsafeReplaceFirstGoal []
+    liftIO $ putStrLn $ "unsafeCheat: " ++ msg
+
+setFocusSide :: Maybe Side -> Proof ()
+setFocusSide x | () <- rnf x = do (_, u) <- Proof ask; liftIO $ modifyIORef u $ \s -> s{focusSide=x}
+
+setFocusAt :: Int -> Proof ()
+setFocusAt !x = do (_, u) <- Proof ask; liftIO $ modifyIORef u $ \s -> s{focusAt=x}
+
+newtype BadProof = BadProof String deriving Typeable
+instance Show BadProof where show (BadProof x) = "Bad proof: " ++ x
+instance Exception BadProof
+
+badProof :: String -> Proof a
+badProof = throwM . BadProof
+
+isBadProof :: Proof () -> Proof Bool
+isBadProof act = C.catch (act >> return False) $ \BadProof{} -> return True
+
+---------------------------------------------------------------------
+-- BINDINGS
+
+newtype Bind a = Bind (Writer [(Var,Exp)] a)
+    deriving (Functor, Applicative, Monad)
+
+addBind :: Var -> Exp -> Bind ()
+addBind a b = Bind $ tell [(a,b)]
+
+runBind :: Bind () -> [(Var,Exp)]
+runBind (Bind x) = execWriter x
diff --git a/src/Proof/Util.hs b/src/Proof/Util.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Util.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE PatternGuards #-}
+
+-- | Generic utilities.
+module Proof.Util(module Proof.Util) where
+
+import System.IO.Unsafe
+import System.Environment
+import Control.DeepSeq
+
+
+rnf2 a b = rnf a `seq` rnf b
+rnf3 a b c = rnf a `seq` rnf b `seq` rnf c
+rnf4 a b c d = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
+rnf5 a b c d e = rnf a `seq` rnf b `seq` rnf c `seq` rnf d `seq` rnf e
+
+headNote note (x:xs) = x
+headNote note [] = error $ "headNote on [], " ++ note
+
+fast = "--fast" `elem` unsafePerformIO getArgs
+
+idempotent :: (Show a, Eq a) => String -> (a -> a) -> (a -> a)
+idempotent name f x0
+    | fast = x1
+    | x1 == x2 = x1
+    | otherwise = error $ unlines
+        ["START Idempotent check failed for " ++ name ++ "!"
+        ,"Input:"
+        ,show x0
+        ,"After first application:"
+        ,show x1
+        ,"After second application:"
+        ,show x2
+        ,"END Idempotent check failed for " ++ name ++ "!"
+        ]
+    where x1 = f x0
+          x2 = f x1
+
+equivalentOn :: (Show a, Show b, Eq b) => (a -> b) -> String -> a -> a -> a
+equivalentOn op name x y
+    | fast = y
+    | xx == yy = y
+    | otherwise = unsafePerformIO $ do
+        writeFile "error.log" $ "-- Equivalent check failed for " ++ name ++ "\n" ++ show x
+        error $ unlines
+            ["START Equivalent check failed for " ++ name ++ "!"
+            ,"Input:"
+            ,show x
+            ,"Output:"
+            ,show y
+            ,"Input (reduced):"
+            ,show xx
+            ,"Output (reduced):"
+            ,show yy
+            ,"END Equivalent check failed for " ++ name ++ "!"
+            ]
+    where xx = op x
+          yy = op y
+
+simpleReadsPrec :: (String -> a) -> (Int -> ReadS a)
+simpleReadsPrec f _ s = [(f s, "")]
diff --git a/test/Classes.hs b/test/Classes.hs
new file mode 100644
--- /dev/null
+++ b/test/Classes.hs
@@ -0,0 +1,131 @@
+
+module Classes(classes) where
+
+import Proof.QED
+import Control.Monad
+
+classes = do
+    lawsMonoid <- laws $ do
+        law "a => a <> mempty = a"
+        law "a => mempty <> a = a"
+        law "a b c => a <> (b <> c) = (a <> b) <> c"
+
+    lawsFunctor <- laws $ do
+        law "fmap id = id"
+        law "f g => fmap f . fmap g = fmap (f . g)"
+
+    lawsApplicative <- laws $ do
+        law "v => pure id <*> v = v"
+        law "u v w => pure (.) <*> u <*> v <*> w = u <*> (v <*> w)"
+        law "f x => pure f <*> pure x = pure (f x)"
+        law "u y => u <*> pure y = pure ($ y) <*> u"
+
+    lawsMonad <- laws $ do
+        law "a k => return a >>= k = k a"
+        law "m => m >>= return = m"
+        law "m k h => m >>= (\\x -> k x >>= h) = (m >>= k) >>= h"
+
+    prove "x => [] ++ x = x" $ do
+        unfold "++"
+
+    prove "x => x ++ [] = x" $ do
+        recurse
+        rhs $ strict "[]"
+
+    prove "x y z => (x ++ y) ++ z = x ++ (y ++ z)" $ do
+        recurse
+        bhs $ unfold "++"
+
+    satisfy "Monoid []" lawsMonoid $ do
+        bind "mempty = []"
+        bind "(<>) = (++)"
+
+    prove "map id = id" $ do
+        bhs $ unfold "id"
+        expand
+        recurse
+        rhs $ strict "[]"
+
+    prove "f g => map f . map g = map (f . g)" $ do
+        twice $ unfold "."
+        twice unlet
+        rhs expand
+        recurse
+        unfold "map"
+
+    satisfy "Functor []" lawsFunctor $ do
+        bind "fmap = map"
+
+    decl "return_List = (:[])"
+    decl "bind_List = flip concatMap"
+    let unwind = mapM_ (perhaps . many . unfold) ["return_List","bind_List","concatMap","concat","flip","."]
+
+    when False $ prove "a k => return_List a `bind_List` k = k a" $ do
+        unwind
+        unfold "map"
+        unfold "foldr"
+        unfold "foldr"
+        unfold "map"
+
+    prove "m => m `bind_List` return_List = m" $ do
+        unwind
+        recurse
+        unfold "map"
+        rhs $ strict "[]"
+        twice $ unfold "++"
+
+    prove "m k h => m `bind_List` (\\x -> k x `bind_List` h) = (m `bind_List` k) `bind_List` h" $ do
+        unwind
+        divide
+        recurse
+        rhs $ unfold "foldr"
+        rhs $ unfold "map"
+        rhs $ unfold "++"
+        unsafeCheat "bored"
+
+    skip $ satisfy "Monad []" lawsMonad $ do
+        bind "return = return_List"
+        bind "(>>=) = bind_List"
+
+    prove "v => return id `ap` v = v" $ do
+        unfold "ap"
+        unfold "liftM2"
+        unfold "$"
+        unsafeCheat "need laws"
+
+{-
+-- (>>=) (return id) (\ b -> (>>=) a (\ c -> return (b c)))    =    a
+--       return a >>= k = k a"
+-- (>>=) a (\ c -> return c))    =    a
+-- a    =    a
+
+data Monad a = Return a | forall x . Bind (Monad x) (x -> Monad a)
+
+eval (Return a) = a
+eval (Bind (Return a) f) = f a
+eval 
+
+-}
+
+    skip $ prove "u v w => return (.) `ap` u `ap` v `ap` w = u `ap` (v `ap` w)" $ do
+        replicateM_ 100 unfold_
+
+    skip $ prove "f x => return f `ap` return x = return (f x)" $ do
+        unfold "ap"
+        unfold "liftM2"
+        unfold "$"
+        unlet
+        return ()
+
+    skip $ do
+        prove "u y => u `ap` return y = return ($ y) `ap` u" $ do
+            return ()
+
+        lawsMonad <- laws $ do
+            law "a k => return a >>= k = k a"
+            law "m => m >>= return = m"
+            law "m k h => m >>= (\\x -> k x >>= h) = (m >>= k) >>= h"
+
+        satisfy "Applicative Monad" lawsApplicative $ do
+            bind "pure = return"
+            bind "(<*>) = ap"
diff --git a/test/HLint.hs b/test/HLint.hs
new file mode 100644
--- /dev/null
+++ b/test/HLint.hs
@@ -0,0 +1,121 @@
+
+module HLint(hlint) where
+
+import Proof.QED
+import Control.Monad.IO.Class
+
+hlint = do
+    decl "data Nat = S Nat | Z"
+    decl "data Int = Neg Nat | Zero | Pos Nat"
+
+    skip $ prove "n x => take n (repeat x) = replicate n x" $ do
+        unfold "replicate"
+
+    skip $ prove "n x => head (drop n x) = x !! n" $ do
+        unfold "head"
+        unfold "error"
+        recurse
+
+
+    prove "f => (($) . f) = f" $ do
+        unfold "$"
+        unfold "."
+        unlet
+        twice $ rhs expand
+
+    prove "f z g x => foldr f z (map g x) = foldr (f . g) z x" $ do
+        unfold "."
+        recurse
+        unfold "map"
+
+    prove "(\\x -> cycle [x]) = repeat" $ do
+        rhs expand
+        recurse
+        unlet
+        twice $ unfold "++"
+
+    prove "f x => zipWith f (repeat x) = map (f x)" $ do
+        expand
+        rhs expand
+        recurse
+        unlet
+        unfold "repeat"
+
+    prove "x y => (if x then False else y) = not x && y" $ do
+        many unfold_
+
+    skip $ prove "map fromJust . filter isJust = catMaybes" $ do
+        unfold "map"
+        unfold "catMaybes"
+        unfold "concatMap"
+        unfold "concat"
+        many $ unfold "."
+        unlet
+        recurse
+        unfold "isJust"
+        unfold "fromJust"
+        bhs $ unfold "map"
+        unfold "++"
+
+    prove "mapMaybe id = catMaybes" $ do
+        unfold "mapMaybe"
+        unfold "."
+        unlet
+        rhs expand
+        divide
+        unfold "id"
+        recurse
+        rhs $ strict "[]"
+
+    prove "f x => map f (repeat x) = repeat (f x)" $ do
+        recurse
+        unfold "repeat"
+        unlet
+
+    prove "f x y => map (uncurry f) (zip x y) = zipWith f x y" $ do
+        unfold "zip"
+        recurse
+        unlet
+        unfold "uncurry"
+        unfold "zipWith"
+        unlet
+        unfold "fst"
+        unfold "snd"
+
+    prove "iterate id = repeat" $ do
+        expand
+        rhs expand
+        recurse
+        at 1 $ unfold "id"
+
+    prove "f x => catMaybes (map f x) = mapMaybe f x" $ do
+        unfold "mapMaybe"
+        unfold "."
+
+    skip $ prove "concatMap maybeToList = catMaybes" $ do
+        unfold "catMaybes"
+        liftIO $ print "here1"
+        expand
+        liftIO $ print "here2"
+        twice divide
+        unfold "maybeToList"
+
+    skip $ prove "f g x => concatMap f (map g x) = concatMap (f . g) x" $ do
+        twice $ unfold "concatMap"
+        twice $ unfold "concat"
+
+    skip $ prove "x => head (reverse x) = last x" $ do
+        unfold "head"
+        unfold "reverse"
+        recurse
+        unlet
+        bhs unfold_
+        unfold "foldl"
+        unlet
+        unfold "flip"
+        error "generalise" -- unsafeReplace "flip (:) [] a" "a"
+        recurse
+        unlet
+        unfold "flip"
+        error "generalise" -- unsafeReplace "flip (:) a b" "a"
+
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,27 @@
+
+module Main(main) where
+
+import Classes
+import HLint
+import Proof.QED
+
+-- TODO: Formalise generalise properly. Can it be done as extraction? Is strict generalisation always sufficient?
+-- TODO: Write an automatic prover
+
+-- TOTHINK: What to do about type classes? How do you prove laws about instances? How do you associate laws?
+--          Add an assume to a proof?
+-- TOTHINK: What do I do about things like +? Do I assume them like I do for type classes?
+-- TOTHINK: Do I just state the laws and leave it at that?
+
+main = qedCheat $ do
+    imports "Builtin"
+    imports "Prelude"
+    imports "List"
+    imports "Maybe"
+    imports "Monad"
+
+    law "a b => a + b = b + a"
+    law "a => a + 0 = a"
+
+    classes
+    hlint