added applysubst function, not yet used in unify function