Module Defun.Open_on_rhs_intf