[NTG-context] A few question about defining symbols and creating downarrow to illustrate function rules