Eq does trivial equality reasoning.
It proves goals of form 
using
hypotheses that are equalities over T and the laws
of reflexivity, commutativity and transitivity.
It also uses hypotheses that are equalities over 
when 
is deducible from other hypotheses using
reflexivity, commutativity and transitivity. The Eq rule
is implemented as a procedure coded in Lisp.