In the process of proving "reftyping-implies-clsmap-result", now still have write and let to do.