adopt same style as E in TSTP proof printing
left equality chaining implemented
passive version of equality chaining implemented
use mandatory renaming everywhere, when applying substitutions