[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)