add subst function and occurs check