proved one case for ref-typing-ok/read