「型消しの言語機能化」って Generalized existentials のことですよね？