diff --git a/ditto.cabal b/ditto.cabal
--- a/ditto.cabal
+++ b/ditto.cabal
@@ -1,5 +1,5 @@
 Name:          ditto
-Version:       0.0.1.1
+Version:       0.1.0.0
 Synopsis:      ditto is a type-safe HTML form generation and validation library
 Description:   ditto follows in the footsteps of formlets and
                digestive-functors <= 0.2. It provides a
@@ -36,6 +36,5 @@
     , mtl              >= 2.0  && < 2.3
     , semigroups       >= 0.16 && < 0.20
     , text             >= 0.11 && < 1.3
-    , bifunctors       >= 5.5  && < 5.7
   hs-source-dirs:      src
 
diff --git a/src/Ditto/Core.hs b/src/Ditto/Core.hs
--- a/src/Ditto/Core.hs
+++ b/src/Ditto/Core.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
 
 {- |
 This module defines the 'Form' type, its instances, core manipulation functions, and a bunch of helper utilities.
@@ -10,7 +10,6 @@
 import Control.Monad.Reader (MonadReader (ask), ReaderT, runReaderT)
 import Control.Monad.State (MonadState (get, put), StateT, evalStateT)
 import Control.Monad.Trans (lift)
-import Data.Biapplicative (Biapplicative ((<<*>>), bipure))
 import Data.Bifunctor (Bifunctor (..))
 import Data.Monoid (Monoid (mappend, mempty))
 import qualified Data.Semigroup as SG
@@ -22,23 +21,21 @@
 ------------------------------------------------------------------------------
 
 -- | Proved records a value, the location that value came from, and something that was proved about the value.
-data Proved proofs a
+data Proved a
   = Proved
-      { proofs :: proofs
-      , pos :: FormRange
+      { pos :: FormRange
       , unProved :: a
       }
   deriving Show
 
-instance Functor (Proved ()) where
-  fmap f (Proved () posi a) = Proved () posi (f a)
+instance Functor Proved where
+  fmap f (Proved posi a) = Proved posi (f a)
 
 -- | Utility Function: trivially prove nothing about ()
-unitProved :: FormId -> Proved () ()
+unitProved :: FormId -> Proved ()
 unitProved formId =
   Proved
-    { proofs = ()
-    , pos = unitRange formId
+    { pos = unitRange formId
     , unProved = ()
     }
 
@@ -168,46 +165,44 @@
 -- @digestive-functors <= 0.2@. If @proof@ is @()@, then 'Form' is an
 -- applicative functor and can be used almost exactly like
 -- @digestive-functors <= 0.2@.
-newtype Form m input error view proof a = Form {unForm :: FormState m input (View error view, m (Result error (Proved proof a)))}
-
-instance (Monad m) => Bifunctor (Form m input view error) where
-  bimap f g (Form frm) =
-    Form $ do
-      (view1, mval) <- frm
-      val <- lift $ lift $ mval
-      case val of
-        (Ok (Proved p posi a)) -> pure (view1, pure $ Ok (Proved (f p) posi (g a)))
-        (Error errs) -> pure (view1, pure $ Error errs)
+newtype Form m input error view a = Form {unForm :: FormState m input (View error view, m (Result error (Proved a)))}
 
-instance (Monoid view, Monad m) => Biapplicative (Form m input error view) where
-  bipure p a =
-    Form $ do
-      i <- getFormId
-      pure (mempty, pure $ Ok (Proved p (unitRange i) a))
+-- instance (Monad m) => Functor (Form m input view error) where
+--   fmap f (Form frm) =
+--     Form $ do
+--       (view1, mval) <- frm
+--       val <- lift $ lift $ mval
+--       case val of
+--         (Ok (Proved posi a)) -> pure (view1, pure $ Ok (Proved posi (f a)))
+--         (Error errs) -> pure (view1, pure $ Error errs)
 
-  (Form frmF) <<*>> (Form frmA) =
-    Form $ do
-      ((view1, mfok), (view2, maok)) <-
-        bracketState $ do
-          res1 <- frmF
-          incFormId
-          res2 <- frmA
-          pure (res1, res2)
-      fok <- lift $ lift $ mfok
-      aok <- lift $ lift $ maok
-      case (fok, aok) of
-        (Error errs1, Error errs2) -> pure (view1 `mappend` view2, pure $ Error $ errs1 ++ errs2)
-        (Error errs1, _) -> pure (view1 `mappend` view2, pure $ Error $ errs1)
-        (_, Error errs2) -> pure (view1 `mappend` view2, pure $ Error $ errs2)
-        (Ok (Proved p (FormRange x _) f), Ok (Proved q (FormRange _ y) a)) ->
-          pure
-            ( view1 `mappend` view2
-            , pure $ Ok $ Proved
-              { proofs = p q
-              , pos = FormRange x y
-              , unProved = f a
-              }
-            )
+-- instance (Monoid view, Monad m) => Applicative (Form m input error view) where
+--   pure a =
+--     Form $ do
+--       i <- getFormId
+--       pure (mempty, pure $ Ok (Proved (unitRange i) a))
+--   (Form frmF) <*> (Form frmA) =
+--     Form $ do
+--       ((view1, mfok), (view2, maok)) <-
+--         bracketState $ do
+--           res1 <- frmF
+--           incFormId
+--           res2 <- frmA
+--           pure (res1, res2)
+--       fok <- lift $ lift $ mfok
+--       aok <- lift $ lift $ maok
+--       case (fok, aok) of
+--         (Error errs1, Error errs2) -> pure (view1 `mappend` view2, pure $ Error $ errs1 ++ errs2)
+--         (Error errs1, _) -> pure (view1 `mappend` view2, pure $ Error $ errs1)
+--         (_, Error errs2) -> pure (view1 `mappend` view2, pure $ Error $ errs2)
+--         (Ok (Proved (FormRange x _) f), Ok (Proved (FormRange _ y) a)) ->
+--           pure
+--             ( view1 `mappend` view2
+--             , pure $ Ok $ Proved
+--               { pos = FormRange x y
+--               , unProved = f a
+--               }
+--             )
 
 bracketState :: Monad m => FormState m input a -> FormState m input a
 bracketState k = do
@@ -217,19 +212,18 @@
   put $ FormRange startF1 endF2
   pure res
 
-instance (Functor m) => Functor (Form m input error view ()) where
+instance (Functor m) => Functor (Form m input error view) where
   fmap f form =
     Form $ fmap (second (fmap (fmap (fmap f)))) (unForm form)
 
-instance (Functor m, Monoid view, Monad m) => Applicative (Form m input error view ()) where
+instance (Functor m, Monoid view, Monad m, x ~ ()) => Applicative (Form m input error view) where
   pure a =
     Form $ do
       i <- getFormId
       pure
         ( View $ const $ mempty
         , pure $ Ok $ Proved
-          { proofs = ()
-          , pos = FormRange i i
+          { pos = FormRange i i
           , unProved = a
           }
         )
@@ -249,12 +243,11 @@
         (Error errs1, Error errs2) -> pure (view1 `mappend` view2, pure $ Error $ errs1 ++ errs2)
         (Error errs1, _) -> pure (view1 `mappend` view2, pure $ Error $ errs1)
         (_, Error errs2) -> pure (view1 `mappend` view2, pure $ Error $ errs2)
-        (Ok (Proved _ (FormRange x _) f), Ok (Proved _ (FormRange _ y) a)) ->
+        (Ok (Proved (FormRange x _) f), Ok (Proved (FormRange _ y) a)) ->
           pure
             ( view1 `mappend` view2
             , pure $ Ok $ Proved
-              { proofs = ()
-              , pos = FormRange x y
+              { pos = FormRange x y
               , unProved = f a
               }
             )
@@ -267,8 +260,8 @@
   :: (Monad m)
   => Environment m input
   -> Text
-  -> Form m input error view proof a
-  -> m (View error view, m (Result error (Proved proof a)))
+  -> Form m input error view a
+  -> m (View error view, m (Result error (Proved a)))
 runForm env prefix' form =
   evalStateT (runReaderT (unForm form) env) (unitRange (zeroId $ unpack prefix'))
 
@@ -278,7 +271,7 @@
   :: (Monad m)
   => Environment m input
   -> Text
-  -> Form m input error view proof a
+  -> Form m input error view a
   -> m (view, Maybe a)
 runForm' env prefix form =
   do
@@ -294,7 +287,7 @@
 viewForm
   :: (Monad m)
   => Text -- ^ form prefix
-  -> Form m input error view proof a -- ^ form to view
+  -> Form m input error view a -- ^ form to view
   -> m view
 viewForm prefix form =
   do
@@ -313,7 +306,7 @@
   :: (Monad m)
   => Environment m input -- ^ Input environment
   -> Text -- ^ Identifier for the form
-  -> Form m input error view proof a -- ^ Form to run
+  -> Form m input error view a -- ^ Form to run
   -> m (Either view a) -- ^ Result
 eitherForm env id' form = do
   (view', mresult) <- runForm env id' form
@@ -328,7 +321,7 @@
 view
   :: (Monad m)
   => view -- ^ View to insert
-  -> Form m input error view () () -- ^ Resulting form
+  -> Form m input error view () -- ^ Resulting form
 view view' =
   Form $ do
     i <- getFormId
@@ -337,8 +330,7 @@
       , pure
         ( Ok
           ( Proved
-            { proofs = ()
-            , pos = FormRange i i
+            { pos = FormRange i i
             , unProved = ()
             }
           )
@@ -354,9 +346,9 @@
 -- element.
 (++>)
   :: (Monad m, Monoid view)
-  => Form m input error view () ()
-  -> Form m input error view proof a
-  -> Form m input error view proof a
+  => Form m input error view ()
+  -> Form m input error view a
+  -> Form m input error view a
 f1 ++> f2 =
   Form $ do
     -- Evaluate the form that matters first, so we have a correct range set
@@ -370,9 +362,9 @@
 --
 (<++)
   :: (Monad m, Monoid view)
-  => Form m input error view proof a
-  -> Form m input error view () ()
-  -> Form m input error view proof a
+  => Form m input error view a
+  -> Form m input error view ()
+  -> Form m input error view a
 f1 <++ f2 =
   Form $ do
     -- Evaluate the form that matters first, so we have a correct range set
@@ -388,8 +380,8 @@
 mapView
   :: (Monad m, Functor m)
   => (view -> view') -- ^ Manipulator
-  -> Form m input error view proof a -- ^ Initial form
-  -> Form m input error view' proof a -- ^ Resulting form
+  -> Form m input error view a -- ^ Initial form
+  -> Form m input error view' a -- ^ Resulting form
 mapView f = Form . fmap (first $ fmap f) . unForm
 
 -- | Utility Function: turn a view and pure value into a successful 'FormState'
@@ -398,15 +390,14 @@
   => FormId
   -> view
   -> a
-  -> FormState m input (View error view, m (Result error (Proved () a)))
+  -> FormState m input (View error view, m (Result error (Proved a)))
 mkOk i view' val =
   pure
     ( View $ const $ view'
     , pure $
       Ok
         ( Proved
-          { proofs = ()
-          , pos = unitRange i
+          { pos = unitRange i
           , unProved = val
           }
         )
diff --git a/src/Ditto/Generalized.hs b/src/Ditto/Generalized.hs
--- a/src/Ditto/Generalized.hs
+++ b/src/Ditto/Generalized.hs
@@ -22,7 +22,7 @@
   => (input -> Either err a)
   -> (FormId -> a -> view)
   -> a
-  -> Form m input err view () a
+  -> Form m input err view a
 input fromInput toView initialValue =
   Form $ do
     i <- getFormId
@@ -34,8 +34,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = initialValue
                 }
               )
@@ -46,8 +45,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = a
                 }
               )
@@ -67,7 +65,7 @@
   => (input -> Either err a)
   -> (FormId -> a -> view)
   -> a
-  -> Form m input err view () (Maybe a)
+  -> Form m input err view (Maybe a)
 inputMaybe fromInput toView initialValue =
   Form $ do
     i <- getFormId
@@ -78,8 +76,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = Just initialValue
                 }
               )
@@ -90,8 +87,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = (Just a)
                 }
               )
@@ -105,8 +101,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = Nothing
                 }
               )
@@ -117,7 +112,7 @@
   :: (Monad m)
   => (FormId -> a -> view)
   -> a
-  -> Form m input err view () ()
+  -> Form m input err view ()
 inputNoData toView a =
   Form $ do
     i <- getFormId
@@ -126,8 +121,7 @@
       , pure $
         Ok
           ( Proved
-            { proofs = ()
-            , pos = unitRange i
+            { pos = unitRange i
             , unProved = ()
             }
           )
@@ -137,7 +131,7 @@
 inputFile
   :: forall m input err view. (Monad m, FormInput input, FormError err, ErrorInputType err ~ input)
   => (FormId -> view)
-  -> Form m input err view () (FileType input)
+  -> Form m input err view (FileType input)
 inputFile toView =
   Form $ do
     i <- getFormId
@@ -154,8 +148,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = a
                 }
               )
@@ -180,7 +173,7 @@
   => [(a, lbl)] -- ^ value, label, initially checked
   -> (FormId -> [(FormId, Int, lbl, Bool)] -> view) -- ^ function which generates the view
   -> (a -> Bool) -- ^ isChecked/isSelected initially
-  -> Form m input err view () [a]
+  -> Form m input err view [a]
 inputMulti choices mkView isSelected =
   Form $ do
     i <- getFormId
@@ -236,7 +229,7 @@
   => (a -> Bool) -- ^ is default
   -> [(a, lbl)] -- ^ value, label
   -> (FormId -> [(FormId, Int, lbl, Bool)] -> view) -- ^ function which generates the view
-  -> Form m input err view () a
+  -> Form m input err view a
 inputChoice isDefault choices mkView =
   Form $ do
     i <- getFormId
@@ -306,11 +299,11 @@
 
 -- | radio buttons, single @\<select\>@ boxes
 inputChoiceForms
-  :: forall a m err input lbl view proof. (Functor m, Monad m, FormError err, ErrorInputType err ~ input, FormInput input)
+  :: forall a m err input lbl view. (Functor m, Monad m, FormError err, ErrorInputType err ~ input, FormInput input)
   => a
-  -> [(Form m input err view proof a, lbl)] -- ^ value, label
+  -> [(Form m input err view a, lbl)] -- ^ value, label
   -> (FormId -> [(FormId, Int, FormId, view, lbl, Bool)] -> view) -- ^ function which generates the view
-  -> Form m input err view proof a
+  -> Form m input err view a
 inputChoiceForms def choices mkView =
   Form $ do
     i <- getFormId -- id used for the 'name' attribute of the radio buttons
@@ -364,27 +357,27 @@
       => FormId
       -> view
       -> a
-      -> FormState m input (View err view, m (Result err (Proved proof a)))
+      -> FormState m input (View err view, m (Result err (Proved a)))
     mkOk' _ view' _ =
       pure
         ( View $ const view'
         , pure $ Error []
         )
-    selectFirst :: [(Form m input err view proof a, lbl)] -> [(Form m input err view proof a, lbl, Bool)]
+    selectFirst :: [(Form m input err view a, lbl)] -> [(Form m input err view a, lbl, Bool)]
     selectFirst ((frm, lbl) : fs) = (frm, lbl, True) : map (\(frm', lbl') -> (frm', lbl', False)) fs
     selectFirst [] = []
-    markSelected :: Either e Int -> [(Int, (Form m input err view proof a, lbl))] -> [(Form m input err view proof a, lbl, Bool)]
+    markSelected :: Either e Int -> [(Int, (Form m input err view a, lbl))] -> [(Form m input err view a, lbl, Bool)]
     markSelected en choices' =
       map (\(i, (f, lbl)) -> (f, lbl, either (const False) (==i) en)) choices'
-    viewSubForm :: (FormId, Int, FormId, Form m input err view proof a, lbl, Bool) -> FormState m input (FormId, Int, FormId, view, lbl, Bool)
+    viewSubForm :: (FormId, Int, FormId, Form m input err view a, lbl, Bool) -> FormState m input (FormId, Int, FormId, view, lbl, Bool)
     viewSubForm (fid, vl, iview, frm, lbl, selected) =
       do
         incFormId
         (v, _) <- unForm frm
         pure (fid, vl, iview, unView v [], lbl, selected)
-    augmentChoices :: (Monad m) => [(Form m input err view proof a, lbl, Bool)] -> FormState m input [(FormId, Int, FormId, Form m input err view proof a, lbl, Bool)]
+    augmentChoices :: (Monad m) => [(Form m input err view a, lbl, Bool)] -> FormState m input [(FormId, Int, FormId, Form m input err view a, lbl, Bool)]
     augmentChoices choices' = mapM augmentChoice (zip [0..] choices')
-    augmentChoice :: (Monad m) => (Int, (Form m input err view proof a, lbl, Bool)) -> FormState m input (FormId, Int, FormId, Form m input err view proof a, lbl, Bool)
+    augmentChoice :: (Monad m) => (Int, (Form m input err view a, lbl, Bool)) -> FormState m input (FormId, Int, FormId, Form m input err view a, lbl, Bool)
     augmentChoice (vl, (frm, lbl, selected)) =
       do
         incFormId
@@ -415,7 +408,7 @@
 label
   :: Monad m
   => (FormId -> view)
-  -> Form m input err view () ()
+  -> Form m input err view ()
 label f =
   Form $ do
     id' <- getFormId
@@ -423,8 +416,7 @@
       ( View (const $ f id')
       , pure
         ( Ok $ Proved
-          { proofs = ()
-          , pos = unitRange id'
+          { pos = unitRange id'
           , unProved = ()
           }
         )
@@ -438,7 +430,7 @@
 errors
   :: Monad m
   => ([err] -> view) -- ^ function to convert the err messages into a view
-  -> Form m input err view () ()
+  -> Form m input err view ()
 errors f =
   Form $ do
     range <- getFormRange
@@ -446,8 +438,7 @@
       ( View (f . retainErrors range)
       , pure
         ( Ok $ Proved
-          { proofs = ()
-          , pos = range
+          { pos = range
           , unProved = ()
           }
         )
@@ -457,7 +448,7 @@
 childErrors
   :: Monad m
   => ([err] -> view)
-  -> Form m input err view () ()
+  -> Form m input err view ()
 childErrors f =
   Form $ do
     range <- getFormRange
@@ -465,8 +456,7 @@
       ( View (f . retainChildErrors range)
       , pure
         ( Ok $ Proved
-          { proofs = ()
-          , pos = range
+          { pos = range
           , unProved = ()
           }
         )
diff --git a/src/Ditto/Generalized/Named.hs b/src/Ditto/Generalized/Named.hs
--- a/src/Ditto/Generalized/Named.hs
+++ b/src/Ditto/Generalized/Named.hs
@@ -23,7 +23,7 @@
   -> (FormId -> a -> view)
   -> a
   -> String
-  -> Form m input err view () a
+  -> Form m input err view a
 input fromInput toView initialValue name =
   Form $ do
     let i = FormIdCustom name
@@ -35,8 +35,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = initialValue
                 }
               )
@@ -47,8 +46,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = a
                 }
               )
@@ -69,7 +67,7 @@
   -> (FormId -> a -> view)
   -> a
   -> String
-  -> Form m input err view () (Maybe a)
+  -> Form m input err view (Maybe a)
 inputMaybe fromInput toView initialValue name =
   Form $ do
     let i = FormIdCustom name
@@ -80,8 +78,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = Just initialValue
                 }
               )
@@ -92,8 +89,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = (Just a)
                 }
               )
@@ -107,8 +103,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = Nothing
                 }
               )
@@ -120,7 +115,7 @@
   => (FormId -> a -> view)
   -> a
   -> String
-  -> Form m input err view () ()
+  -> Form m input err view ()
 inputNoData toView a name =
   Form $ do
     let i = FormIdCustom name
@@ -129,8 +124,7 @@
       , pure $
         Ok
           ( Proved
-            { proofs = ()
-            , pos = unitRange i
+            { pos = unitRange i
             , unProved = ()
             }
           )
@@ -141,7 +135,7 @@
   :: forall m input err view. (Monad m, FormInput input, FormError err, ErrorInputType err ~ input)
   => (FormId -> view)
   -> String
-  -> Form m input err view () (FileType input)
+  -> Form m input err view (FileType input)
 inputFile toView name =
   Form $ do
     let i = FormIdCustom name
@@ -158,8 +152,7 @@
           , pure $
             Ok
               ( Proved
-                { proofs = ()
-                , pos = unitRange i
+                { pos = unitRange i
                 , unProved = a
                 }
               )
@@ -185,7 +178,7 @@
   -> (FormId -> [(FormId, Int, lbl, Bool)] -> view) -- ^ function which generates the view
   -> (a -> Bool) -- ^ isChecked/isSelected initially
   -> String
-  -> Form m input err view () [a]
+  -> Form m input err view [a]
 inputMulti choices mkView isSelected name =
   Form $ do
     let i = FormIdCustom name
@@ -242,7 +235,7 @@
   -> [(a, lbl)] -- ^ value, label
   -> (FormId -> [(FormId, Int, lbl, Bool)] -> view) -- ^ function which generates the view
   -> String
-  -> Form m input err view () a
+  -> Form m input err view a
 inputChoice isDefault choices mkView name =
   Form $ do
     let i = FormIdCustom name
@@ -312,12 +305,12 @@
 
 -- | radio buttons, single @\<select\>@ boxes
 inputChoiceForms
-  :: forall a m err input lbl view proof. (Functor m, Monad m, FormError err, ErrorInputType err ~ input, FormInput input)
+  :: forall a m err input lbl view. (Functor m, Monad m, FormError err, ErrorInputType err ~ input, FormInput input)
   => a
-  -> [(Form m input err view proof a, lbl)] -- ^ value, label
+  -> [(Form m input err view a, lbl)] -- ^ value, label
   -> (FormId -> [(FormId, Int, FormId, view, lbl, Bool)] -> view) -- ^ function which generates the view
   -> String
-  -> Form m input err view proof a
+  -> Form m input err view a
 inputChoiceForms def choices mkView name =
   Form $ do
     let i = FormIdCustom name -- id used for the 'name' attribute of the radio buttons
@@ -371,27 +364,27 @@
       => FormId
       -> view
       -> a
-      -> FormState m input (View err view, m (Result err (Proved proof a)))
+      -> FormState m input (View err view, m (Result err (Proved a)))
     mkOk' _ view' _ =
       pure
         ( View $ const view'
         , pure $ Error []
         )
-    selectFirst :: [(Form m input err view proof a, lbl)] -> [(Form m input err view proof a, lbl, Bool)]
+    selectFirst :: [(Form m input err view a, lbl)] -> [(Form m input err view a, lbl, Bool)]
     selectFirst ((frm, lbl) : fs) = (frm, lbl, True) : map (\(frm', lbl') -> (frm', lbl', False)) fs
     selectFirst [] = []
-    markSelected :: Either e Int -> [(Int, (Form m input err view proof a, lbl))] -> [(Form m input err view proof a, lbl, Bool)]
+    markSelected :: Either e Int -> [(Int, (Form m input err view a, lbl))] -> [(Form m input err view a, lbl, Bool)]
     markSelected en choices' =
       map (\(i, (f, lbl)) -> (f, lbl, either (const False) (==i) en)) choices'
-    viewSubForm :: (FormId, Int, FormId, Form m input err view proof a, lbl, Bool) -> FormState m input (FormId, Int, FormId, view, lbl, Bool)
+    viewSubForm :: (FormId, Int, FormId, Form m input err view a, lbl, Bool) -> FormState m input (FormId, Int, FormId, view, lbl, Bool)
     viewSubForm (fid, vl, iview, frm, lbl, selected) =
       do
         incFormId
         (v, _) <- unForm frm
         pure (fid, vl, iview, unView v [], lbl, selected)
-    augmentChoices :: (Monad m) => [(Form m input err view proof a, lbl, Bool)] -> FormState m input [(FormId, Int, FormId, Form m input err view proof a, lbl, Bool)]
+    augmentChoices :: (Monad m) => [(Form m input err view a, lbl, Bool)] -> FormState m input [(FormId, Int, FormId, Form m input err view a, lbl, Bool)]
     augmentChoices choices' = mapM augmentChoice (zip [0..] choices')
-    augmentChoice :: (Monad m) => (Int, (Form m input err view proof a, lbl, Bool)) -> FormState m input (FormId, Int, FormId, Form m input err view proof a, lbl, Bool)
+    augmentChoice :: (Monad m) => (Int, (Form m input err view a, lbl, Bool)) -> FormState m input (FormId, Int, FormId, Form m input err view a, lbl, Bool)
     augmentChoice (vl, (frm, lbl, selected)) =
       do
         incFormId
@@ -422,7 +415,7 @@
 label
   :: Monad m
   => (FormId -> view)
-  -> Form m input err view () ()
+  -> Form m input err view ()
 label f =
   Form $ do
     id' <- getFormId
@@ -430,8 +423,7 @@
       ( View (const $ f id')
       , pure
         ( Ok $ Proved
-          { proofs = ()
-          , pos = unitRange id'
+          { pos = unitRange id'
           , unProved = ()
           }
         )
@@ -445,7 +437,7 @@
 errors
   :: Monad m
   => ([err] -> view) -- ^ function to convert the err messages into a view
-  -> Form m input err view () ()
+  -> Form m input err view ()
 errors f =
   Form $ do
     range <- getFormRange
@@ -453,8 +445,7 @@
       ( View (f . retainErrors range)
       , pure
         ( Ok $ Proved
-          { proofs = ()
-          , pos = range
+          { pos = range
           , unProved = ()
           }
         )
@@ -464,7 +455,7 @@
 childErrors
   :: Monad m
   => ([err] -> view)
-  -> Form m input err view () ()
+  -> Form m input err view ()
 childErrors f =
   Form $ do
     range <- getFormRange
@@ -472,8 +463,7 @@
       ( View (f . retainChildErrors range)
       , pure
         ( Ok $ Proved
-          { proofs = ()
-          , pos = range
+          { pos = range
           , unProved = ()
           }
         )
diff --git a/src/Ditto/Proof.hs b/src/Ditto/Proof.hs
--- a/src/Ditto/Proof.hs
+++ b/src/Ditto/Proof.hs
@@ -10,7 +10,6 @@
 module Ditto.Proof where
 
 import Control.Monad.Trans (lift)
-import Data.Bifunctor (Bifunctor (bimap))
 import Numeric (readDec, readFloat, readSigned)
 import Ditto.Core (Form (..), Proved (..))
 import Ditto.Result (Result (..))
@@ -23,27 +22,24 @@
 -- Generally, each 'Proof' has a unique data-type associated with it
 -- which names the proof, such as:
 --
--- > data NotNull = NotNull
 --
-data Proof m error proof a b
-  = Proof
-      { proofName :: proof -- ^ name of the thing to prove
-      , proofFunction :: a -> m (Either error b) -- ^ function which provides the proof
-      }
+data Proof m error a b = Proof
+  { proofFunction :: a -> m (Either error b) -- ^ function which provides the proof
+  }
 
 -- | apply a 'Proof' to a 'Form'
 prove
   :: (Monad m)
-  => Form m input error view q a
-  -> Proof m error proof a b
-  -> Form m input error view proof b
-prove (Form frm) (Proof p f) =
+  => Form m input error view a
+  -> Proof m error a b
+  -> Form m input error view b
+prove (Form frm) (Proof f) =
   Form $ do
     (xml, mval) <- frm
     val <- lift $ lift $ mval
     case val of
       (Error errs) -> pure (xml, pure $ Error errs)
-      (Ok (Proved _ posi a)) ->
+      (Ok (Proved posi a)) ->
         do
           r <- lift $ lift $ f a
           case r of
@@ -54,8 +50,7 @@
                 , pure $
                   Ok
                     ( Proved
-                      { proofs = p
-                      , pos = posi
+                      { pos = posi
                       , unProved = b
                       }
                     )
@@ -68,56 +63,44 @@
 -- This is useful when you want just want classic digestive-functors behaviour.
 transform
   :: (Monad m)
-  => Form m input error view anyProof a
-  -> Proof m error proof a b
-  -> Form m input error view () b
-transform frm proof = bimap (const ()) id (frm `prove` proof)
+  => Form m input error view a
+  -> Proof m error a b
+  -> Form m input error view b
+transform frm proof = frm `prove` proof
 
 -- | transform the 'Form' result using a monadic 'Either' function.
 transformEitherM
   :: (Monad m)
-  => Form m input error view anyProof a
+  => Form m input error view a
   -> (a -> m (Either error b))
-  -> Form m input error view () b
-transformEitherM frm func = frm `transform` (Proof () func)
+  -> Form m input error view b
+transformEitherM frm func = frm `transform` (Proof func)
 
 -- | transform the 'Form' result using an 'Either' function.
 transformEither
   :: (Monad m)
-  => Form m input error view anyProof a
+  => Form m input error view a
   -> (a -> Either error b)
-  -> Form m input error view () b
+  -> Form m input error view b
 transformEither frm func = transformEitherM frm (pure . func)
 
 -- * Various Proofs
 
--- | proof that a list is not empty
-data NotNull = NotNull
-
 -- | prove that a list is not empty
-notNullProof :: (Monad m) => error -> Proof m error NotNull [a] [a]
-notNullProof errorMsg = Proof NotNull (pure . check)
+notNullProof :: (Monad m) => error -> Proof m error [a] [a]
+notNullProof errorMsg = Proof (pure . check)
   where
     check list =
       if null list
       then (Left errorMsg)
       else (Right list)
 
--- | proof that a 'String' is a decimal number
-data Decimal = Decimal
-
--- | proof that a 'String' is a Real/Fractional number
-data RealFractional = RealFractional
-
--- | proof that a number is also (allowed to be) signed
-data Signed a = Signed a
-
 -- | read an unsigned number in decimal notation
 decimal
   :: (Monad m, Eq i, Num i)
   => (String -> error) -- ^ create an error message ('String' is the value that did not parse)
-  -> Proof m error Decimal String i
-decimal mkError = Proof Decimal (pure . toDecimal)
+  -> Proof m error String i
+decimal mkError = Proof (pure . toDecimal)
   where
     toDecimal str =
       case readDec str of
@@ -125,8 +108,8 @@
         _ -> (Left $ mkError str)
 
 -- | read signed decimal number
-signedDecimal :: (Monad m, Eq i, Real i) => (String -> error) -> Proof m error (Signed Decimal) String i
-signedDecimal mkError = Proof (Signed Decimal) (pure . toDecimal)
+signedDecimal :: (Monad m, Eq i, Real i) => (String -> error) -> Proof m error String i
+signedDecimal mkError = Proof (pure . toDecimal)
   where
     toDecimal str =
       case (readSigned readDec) str of
@@ -134,8 +117,8 @@
         _ -> (Left $ mkError str)
 
 -- | read 'RealFrac' number
-realFrac :: (Monad m, RealFrac a) => (String -> error) -> Proof m error RealFractional String a
-realFrac mkError = Proof RealFractional (pure . toRealFrac)
+realFrac :: (Monad m, RealFrac a) => (String -> error) -> Proof m error String a
+realFrac mkError = Proof (pure . toRealFrac)
   where
     toRealFrac str =
       case readFloat str of
@@ -143,8 +126,8 @@
         _ -> (Left $ mkError str)
 
 -- | read a signed 'RealFrac' number
-realFracSigned :: (Monad m, RealFrac a) => (String -> error) -> Proof m error (Signed RealFractional) String a
-realFracSigned mkError = Proof (Signed RealFractional) (pure . toRealFrac)
+realFracSigned :: (Monad m, RealFrac a) => (String -> error) -> Proof m error String a
+realFracSigned mkError = Proof (pure . toRealFrac)
   where
     toRealFrac str =
       case (readSigned readFloat) str of
diff --git a/src/Ditto/Result.hs b/src/Ditto/Result.hs
--- a/src/Ditto/Result.hs
+++ b/src/Ditto/Result.hs
@@ -20,7 +20,6 @@
 import Control.Applicative (Applicative (..))
 import Data.List.NonEmpty (NonEmpty(..))
 import qualified Data.List.NonEmpty as NE
--- import Data.List (intercalate)
 
 -- | Type for failing computations
 --
@@ -87,7 +86,8 @@
 
 -- | get the head 'Integer' from a 'FormId'
 formId :: FormId -> Integer
-formId = NE.head . formIdList
+formId (FormId _ (x :| _)) = x
+formId (FormIdCustom x) = fromIntegral $ sum $ fromEnum <$> x
 
 -- | A range of ID's to specify a group of forms
 --