Problem 2 [12pt] Consider the simply typed A-calculus and its typing rules defined in Note 3. Suppose we want to add a new operation e, which performs the "Xor" operation on two booleans, we can define the syntax of this new language as follows: terms ee1 e2 where the dots represents the terms defined in note 3. The syntax of types remains unchanged. a) (4pt) Follow the notations in Note 3, write down a typing rule (call it TXor) for the new term el # e2. b) (8pt) What is the type of the term ((Az: bool. (z # (true ^ false)) true)? Justify your answer by writing down the proof tree for this term