Some tools for computer-assisted theorem proving in Martin-L"of type theory
Marcin Benke · 2001
Abstract. We propose some tools facilitating interactive proof and program development in the proof editor Alfa based on Martin-Löf Type Theory, in particular a tool for equality reasoning supported by tools for deriving equality (and proofs or its properties) for inductive datatypes as well as automated proof-search. 1