Try adding a language with proof solving capabilities. ATS, Agda, Idris, Coq spring to mind.