I've really liked educational proof checkers going back to the tutch proof checker. One thing I didn't see here is the ability to header-like file which declar

I've really liked educational proof checkers going back to the tutch proof checker. One thing I didn't see here is the ability to header-like file which declares the type of proofs... the syntax of deduce looks very nice though.