Here, a notation of the form <math>x \underset{A}{\Downarrow}</math> means that <math>x\!</math> is of the type <math>A,\!</math> while a notation of the form <math>x \overset{A}{\underset{B}{\Downarrow}}</math> means that <math>x\!</math> is of the type <math>A \Rightarrow B.</math> | Here, a notation of the form <math>x \underset{A}{\Downarrow}</math> means that <math>x\!</math> is of the type <math>A,\!</math> while a notation of the form <math>x \overset{A}{\underset{B}{\Downarrow}}</math> means that <math>x\!</math> is of the type <math>A \Rightarrow B.</math> |