moved some code and refactored substitution in termination proof
use sameOpSymbs instead of equality, too