  Mella is a minimalistic dependently typed programming language and
interactive theorem prover implemented in Haskell. Its main purpose is to
investigate the effective integration of automated theorem provers in a pure
and simple setting. Such integrations are essential for supporting program
development in dependently typed languages. We integrate the equational theorem
prover Waldmeister and test it on more than 800 proof goals from the TPTP
library. In contrast to previous approaches, the reconstruction of Waldmeister
proofs within Mella is quite robust and does not generate a significant
overhead to proof search. Mella thus yields a template for integrating more
expressive theorem provers in more sophisticated languages.
