보기 좋게 식의 문자 바꾸기.

changevar(exp, rel, new, old)
예를 들어,

 changevar(y, j=k+1, j, k) 하면,

함수의 정의, 가정

f(x) := ...
fundef(f) Not fundef(f(x))
dispfun(f,g), dispfun(all)
assume() <---> forget(), facts()로 확인.