Here is the complete grammar.

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

The comments for A1Q2 still apply.

To submit: A2Q1.rkt