get' :: Maybe a -> a
get' (Just x) = x
get' Nothing = undefined

reduce :: Expr -> Expr
reduce e = get' ((reduce <$> reduceOnce e) <|> Just e)

nf :: Expr -> Expr
nf (Var x) = Var x
nf e@(e1 :@ e2) = reduce ((nf e1) :@ (nf e2))
nf e@(Lam s e1) = reduce (Lam s (nf e1))