diff --git a/bench/gps.txt b/bench/gps.txt
--- a/bench/gps.txt
+++ b/bench/gps.txt
@@ -336,7 +336,7 @@
 -- 0 candidates of size 3
 -- 10 candidates of size 4
 -- tested 10 candidates
-gps18 xs ys  =  zipWith (+) xs ys
+gps18  =  zipWith (+)
 
 gps19 :: Int -> [Char] -> [Char]
 -- testing 3 combinations of argument values
diff --git a/bench/gps2.txt b/bench/gps2.txt
--- a/bench/gps2.txt
+++ b/bench/gps2.txt
@@ -94,7 +94,7 @@
 -- 0 candidates of size 2
 -- 1 candidates of size 3
 -- tested 2 candidates
-gps5 x  =  tell [25,10,5,1] x
+gps5  =  tell [25,10,5,1]
 
 gps5 :: Int -> [Int]
 -- testing 6 combinations of argument values
@@ -111,7 +111,7 @@
 -- 9232 candidates of size 10
 -- 43847 candidates of size 11
 -- tested 32290 candidates
-gps5 x  =  tell [25,10,5,1] x
+gps5  =  tell [25,10,5,1]
 
 gps6 :: [Int] -> Int
 -- testing 360 combinations of argument values
diff --git a/bench/runtime/zero/eg/setelem.runtime b/bench/runtime/zero/eg/setelem.runtime
--- a/bench/runtime/zero/eg/setelem.runtime
+++ b/bench/runtime/zero/eg/setelem.runtime
@@ -1,1 +1,1 @@
-1.4
+2.1
diff --git a/bench/terpret.txt b/bench/terpret.txt
--- a/bench/terpret.txt
+++ b/bench/terpret.txt
@@ -168,5 +168,5 @@
 -- 2 candidates of size 3
 -- 2 candidates of size 4
 -- tested 6 candidates
-decrelements xs  =  map (subtract 1) xs
+decrelements  =  map (subtract 1)
 
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,13 @@
 ============================
 
 
+v0.7.2 (May 2025)
+-----------------
+
+* Add `unfun` as a potential future replacement for `con`.
+* eta-reduce when applicable before displaying result
+
+
 v0.7.0 (May 2025)
 -----------------
 
diff --git a/code-conjure.cabal b/code-conjure.cabal
--- a/code-conjure.cabal
+++ b/code-conjure.cabal
@@ -3,7 +3,7 @@
 -- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 name:                code-conjure
-version:             0.7.0
+version:             0.7.2
 synopsis:            synthesize Haskell functions out of partial definitions
 description:
   Conjure is a tool that synthesizes Haskell functions out of partial definitions.
@@ -69,7 +69,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.7.0
+  tag:             v0.7.2
 
 library
   exposed-modules: Conjure
diff --git a/eg/bools.txt b/eg/bools.txt
--- a/eg/bools.txt
+++ b/eg/bools.txt
@@ -30,7 +30,7 @@
 -- 0 candidates of size 3
 -- 4 candidates of size 4
 -- tested 6 candidates
-and ps  =  foldr (&&) True ps
+and  =  foldr (&&) True
 
 or :: [Bool] -> Bool
 -- testing 14 combinations of argument values
@@ -40,5 +40,5 @@
 -- 0 candidates of size 3
 -- 4 candidates of size 4
 -- tested 5 candidates
-or ps  =  foldr (||) False ps
+or  =  foldr (||) False
 
diff --git a/eg/ints.txt b/eg/ints.txt
--- a/eg/ints.txt
+++ b/eg/ints.txt
@@ -49,7 +49,7 @@
 -- 0 candidates of size 3
 -- 3 candidates of size 4
 -- tested 3 candidates
-sum xs  =  foldr (+) 0 xs
+sum  =  foldr (+) 0
 
 product :: [Int] -> Int
 -- testing 360 combinations of argument values
@@ -59,5 +59,5 @@
 -- 0 candidates of size 3
 -- 3 candidates of size 4
 -- tested 5 candidates
-product xs  =  foldr (*) 1 xs
+product  =  foldr (*) 1
 
diff --git a/eg/setelem.hs b/eg/setelem.hs
--- a/eg/setelem.hs
+++ b/eg/setelem.hs
@@ -5,36 +5,37 @@
 import Conjure
 
 elem' :: Int -> [Int] -> Bool
-elem' x [y]  =  x == y
-elem' x [y,z]  =  x == y || x == z
-elem' x [y,z,w]  =  x == y || x == z || x == w
+elem' 0 [1]  =  False
+elem' 1 [1,2]  =  True
+elem' 0 [1,2]  =  False
+elem' 2 [0,1,2]  =  True
 
 set' :: [Int] -> Bool
-set' []  =  True
-set' [x]  =  True
-set' [x,y]  =  not (x == y)
-set' [x,y,z]  =  not (x == y || y == z || x == z)
+set' [1,1]  =  False
+set' [1,2]  =  True
+set' [1,0,0]  =  False
+set' [1,2,3]  =  True
 
 main :: IO ()
 main = do
   conjure "elem" (elem')
-    [ con ([] :: [Int])
-    , con True
+    [ con True
     , con False
     , fun "||" (||)
     , fun "&&" (&&)
     , fun "not" not
+    , con ([] :: [Int])
     , fun ":" ((:) :: Int -> [Int] -> [Int])
     , fun "==" ((==) :: Int -> Int -> Bool)
     ]
 
   conjure "set" (set')
-    [ con ([] :: [Int])
-    , con True
+    [ con True
     , con False
-    , fun "&&" (&&)
     , fun "||" (||)
+    , fun "&&" (&&)
     , fun "not" not
+    , con ([] :: [Int])
     , fun ":" ((:) :: Int -> [Int] -> [Int])
     , fun "elem" (elem :: Int -> [Int] -> Bool)
     ]
diff --git a/eg/setelem.txt b/eg/setelem.txt
--- a/eg/setelem.txt
+++ b/eg/setelem.txt
@@ -1,5 +1,5 @@
 elem :: Int -> [Int] -> Bool
--- testing 360 combinations of argument values
+-- testing 4 combinations of argument values
 -- pruning with 40/53 rules
 -- 2 candidates of size 1
 -- 0 candidates of size 2
@@ -14,17 +14,17 @@
 elem x (y:xs)  =  x == y || elem x xs
 
 set :: [Int] -> Bool
--- testing 360 combinations of argument values
+-- testing 4 combinations of argument values
 -- pruning with 41/52 rules
 -- 2 candidates of size 1
 -- 0 candidates of size 2
 -- 0 candidates of size 3
--- 1 candidates of size 4
+-- 2 candidates of size 4
 -- 0 candidates of size 5
 -- 0 candidates of size 6
--- 2 candidates of size 7
--- 4 candidates of size 8
--- tested 6 candidates
+-- 4 candidates of size 7
+-- 8 candidates of size 8
+-- tested 10 candidates
 set []  =  True
 set (x:xs)  =  not (elem x xs) && set xs
 
diff --git a/eg/sort.txt b/eg/sort.txt
--- a/eg/sort.txt
+++ b/eg/sort.txt
@@ -18,7 +18,7 @@
 -- 0 candidates of size 3
 -- 2 candidates of size 4
 -- tested 4 candidates
-sort xs  =  foldr insert [] xs
+sort  =  foldr insert []
 
 insert :: Int -> [Int] -> [Int]
 -- testing 4 combinations of argument values
diff --git a/eg/tapps.txt b/eg/tapps.txt
--- a/eg/tapps.txt
+++ b/eg/tapps.txt
@@ -28,5 +28,5 @@
 -- 1 candidates of size 3
 -- 5 candidates of size 4
 -- tested 8 candidates
-product xs  =  foldr (*) 1 xs
+product  =  foldr (*) 1
 
diff --git a/src/Conjure.hs b/src/Conjure.hs
--- a/src/Conjure.hs
+++ b/src/Conjure.hs
@@ -96,6 +96,7 @@
     conjure
   , Ingredient
   , con
+  , unfun
   , fun
   , guard
   , iif
diff --git a/src/Conjure/Defn.hs b/src/Conjure/Defn.hs
--- a/src/Conjure/Defn.hs
+++ b/src/Conjure/Defn.hs
@@ -32,6 +32,8 @@
   , isBaseCase
   , isRecursiveCase
   , isRecursiveDefn
+  , caneta
+  , etaReduce
   , module Conjure.Expr
   )
 where
@@ -39,6 +41,7 @@
 import Conjure.Utils
 import Conjure.Expr
 import Data.Express.Utils.Typeable (boolTy, orderingTy)
+import Data.Express.Utils.String (isInfix)
 import Data.Dynamic
 -- import Control.Applicative ((<$>)) -- for older GHCs
 
@@ -327,3 +330,26 @@
 -- | Returns whether a definition is recursive
 isRecursiveDefn :: Defn -> Bool
 isRecursiveDefn  =  any isRecursiveCase
+
+-- | Returns whether eta-reduction is possible in the given 'Bndn'
+--
+-- This says 'False' to some cases that are eta-reducible but would yield ugly results
+caneta :: Bndn -> Bool
+caneta (_, Value "if" _ :$ _ :$ _ :$ _)          =  False
+caneta (_, Value "|" _ :$ _ :$ _ :$ _)           =  False
+caneta (_, Value "case" _ :$ _ :$ _ :$ _ :$ _)   =  False
+caneta (Value (_:s) _ :$ _ :$ _, _) | isInfix s  =  False
+caneta (_, Value s _ :$ _ :$ _)     | isInfix s  =  False
+caneta (elf :$ elx, erf :$ erx)  =  elx == erx && erx `notElem` values erf
+caneta _  =  False
+
+
+-- | When possible, performs eta-reduction in the given definition
+etaReduce :: Defn -> Defn
+etaReduce  =  try
+  where
+  try d
+    | all caneta d  =  try $ map reduce d
+    | otherwise     =  d
+  reduce (lhs :$ _, rhs :$ _)  =  (lhs, rhs)
+  reduce _  =  error "Conjure.Defn.etaReduce: the impossible happened, this is a bug"
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -223,7 +223,7 @@
       let (cs',cs'') = break (i==) cs
       let t' = t + length cs' + 1
       putWithTimeSince t0 $ "tested " ++ show t' ++ " candidates"
-      putStrLn $ showDefn $ normalizeDefn thy i
+      putStrLn $ showDefn $ etaReduce $ normalizeDefn thy i
       when carryOn $ pr1 t' is (drop 1 cs'')
   rs  =  zip iss css
   results  =  conjpure0 nm f p es
diff --git a/src/Conjure/Ingredient.hs b/src/Conjure/Ingredient.hs
--- a/src/Conjure/Ingredient.hs
+++ b/src/Conjure/Ingredient.hs
@@ -12,6 +12,7 @@
 module Conjure.Ingredient
   ( Ingredient
   , con
+  , unfun
   , fun
   , iif
   , ordcase
@@ -82,10 +83,32 @@
 con x  =  (val x, conjureType x)
 
 
+-- | Provided a 'Show'-able non-functional value to Conjure.
+--   (cf. 'fun')
+--
+-- > conjure "foo" foo [ unfun False
+-- >                   , unfun True
+-- >                   , unfun (0 :: Int)
+-- >                   , unfun (1 :: Int)
+-- >                   , ...
+-- >                   ]
+--
+-- Argument types have to be monomorphized,
+-- so use type bindings when applicable.
+--
+-- TODO:  Make 'unfun' the standard way to create encode 'Show' values.
+--
+-- This is a replacement to 'con'.
+-- In hindsight, 'con' is not such a great name:
+-- 'con'structors may be 'fun'ctional after all!
+unfun :: (Conjurable a, Show a) => a -> Ingredient
+unfun x  =  (val x, conjureType x)
+
+
 -- | Provides a functional value as an ingredient to Conjure.
 --   To be used on values that are not 'Show' instances
 --   such as functions.
---   (cf. 'con')
+--   (cf. 'unfun', 'con')
 --
 -- > conjure "foo" foo [ ...
 -- >                   , fun "&&" (&&)
diff --git a/test/defn.hs b/test/defn.hs
--- a/test/defn.hs
+++ b/test/defn.hs
@@ -212,6 +212,18 @@
     ++ "             LT -> False\n"
     ++ "             EQ -> True\n"
     ++ "             GT -> False\n"
+
+  , caneta (ff xx, zero) == False
+  , caneta (ff xx, gg xx) == True
+  , caneta (ff xx, one -+- two) == False
+  , caneta (ff xx, one -+- xx) == False -- we don't eta-reduce infix ops
+  , caneta (ff xx, xx -+- one) == False
+  , caneta (ff2 xx yy, xx -+- yy) == False -- we don't eta-reduce infix ops
+  , caneta (ff2 xx yy, one -+- yy) == False -- we don't eta-reduce infix ops
+  , caneta (ff2 xx yy, ff2 xx yy) == True
+  , caneta (ff2 xx yy, ff2 one yy) == True
+
+  , etaReduce [(ff xx, gg xx)] == [(ffE, ggE)]
   ]
 
 dvl :: Typeable a => Defn -> Expr -> a