Provide an explicit proof, for example chaining equalities
Dft is a proof-checking-like macro that allows you to chain
together equalities. The name "dft" is short for "defthm". In
the community-books see books/misc/dft-ex.lisp for some
examples.
This tool has not been used in big proofs and probably can be improved
quite a bit. The author encourages users to build improved versions.
