fixing the automation for MonadExpr.
new proofs for SetoidFold.