betaReduce = untilStable betaReduce1
         
betaReduce1 = everywhere' (mkT f)
    where
      f (AppE (LamE [VarP x]    e) z)  = subst x z e
      f (AppE (LamE (VarP x:ps) e) z) = subst x z (LamE ps e)
      f a = a


subst x replacement = everywhere (mkT f)
    where
      f (VarE x1) | x1 == x = replacement 
      f a = a


untilStable f x = go x where
  go x = case f x of
           x1 | x1 == x -> x
           x1 -> go (f x)