Is there an software package aimed at verfication of simple equational proofs? I am hoping to avoid the usual overhead involved with First Order Logic or Higher Order Logic verification systems. ...
Technically, it is possible to prove anything in Coq proof assistant  (on at least Linux) due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis ...