diff --git a/Proof/Propositional.hs b/Proof/Propositional.hs
--- a/Proof/Propositional.hs
+++ b/Proof/Propositional.hs
@@ -8,7 +8,7 @@
        ( type (/\), type (\/), Not, exfalso, orIntroL
        , orIntroR, orElim, andIntro, andElimL
        , andElimR, orAssocL, orAssocR
-       , andAssocL, andAssocR, IsTrue(..)
+       , andAssocL, andAssocR, IsTrue(..), withWitness
        , Empty(..), withEmpty, withEmpty'
        , refute
        , Inhabited (..), withInhabited
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -2,7 +2,7 @@
 --  documentation, see http://haskell.org/cabal/users-guide/
 
 name:                equational-reasoning
-version:             0.4.1.0
+version:             0.4.1.1
 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
 description:         A simple convenient library to write equational / preorder proof as in Agda.
 license:             BSD3