Equational Reasoning Assistant (ERA)
is a syntax manipulation tool that allows
users to do equational reasoning on Haskell programs.
It has a graphical interface, letting users point
and click on expressions (or sub-expressions),
and transform these expressions in well defined ways.
ERA comes with a large library of lemmas about
Haskell prelude functions. When released, Era will
also have a proof butler that will help with
typesetting the proofs that the user has performed.