Here is the complete grammar.

expr = (λ x => expr)
     | (∧-intro expr expr)
     | (∧-elim0 expr)
     | (∧-elim1 expr)
     | (expr expr)
     | (expr : type)
     | ?
     | x
 	 	 	 	 
type = (type -> type)
     | (type ∧ type)
     | X

You will have to create new AST structures, extend the parser and
pretty-printer (always think carefully about the order in which you do
pattern matching, as there can be overlap in patterns) and extend the
type-check and type-synth functions, as well as the functions
replace-goal-with and number-new-holes.

The sequence of questions in the first three assignments is
cumulative, in the sense that each programming question builds on the
previous one.  Here is one possible approach to them. Implement the
rules for this question, then test your code by doing the next
question, which involves using the new features to do proofs (also
think of additional expressions of your own choosing, because that's
not enough testing). Submit this question when you think your code has
been tested, then submit the next question. Continue in this fashion
for the other questions, using the proof questions as a starting point
for the tests for the programming that implements the new features
used in the proof questions.  Constantly extend your test set so that
earlier tests are repeated for later additions, to make sure you
haven't broken anything.  (You don't have to do it this way if you
don't want to.)

You are free to change the error messages to give yourself more
information in debugging either your code or your proofs, but please
make sure that the error messages contain the letter sequences "check"
and "synth" for errors in type checking and type synthesis mode
respectively.

To submit: A1Q2.rkt