Here is the complete grammar.

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

The comments for A1Q2 still apply, except that you don't have to
create new AST structures for ¬, because (¬ T) is desugared to
(T -> ⊥) in the parser. Leave it like this in the pretty-printer, don't
resugar it. That makes interactive development a bit easier at the
beginning.

To submit: A3Q1.rkt