Catch empty lambda in map

diff --git a/SimpleFT.hs b/SimpleFT.hs
index 9589bcf..12585dc 100644 (file)
--- a/SimpleFT.hs
+++ b/SimpleFT.hs
@@ -22,11 +22,12 @@ freeTheorem' e1 e2 (List t) = do
        [v1,v2] <- asks (take 2)
        local (drop 2) $ do
                map <- freeTheorem' (Var v1) (Var v2) t
-               case map of
-                 (Equal (Var v1') ev1) | v1' == v1 -> do
-                       return $ Equal e1 (App (App (Var "map") (lambda v2 ev1)) e2)
-                 _ -> do
-                       return $ Pairwise v1 v2 map e1 e2
+               return $ case map of
+                 (Equal (Var v1') ev1) | v1' == v1 -> 
+                       if ev1 == (Var v2)
+                       then Equal e1 e2
+                       else Equal e1 (App (App (Var "map") (lambda v2 ev1)) e2)
+                 _ ->       Pairwise v1 v2 map e1 e2
 
 freeTheorem' e1 e2 (Arrow t1 t2) = do
        [v1,v2] <- asks (take 2)