Here is the complete grammar.

expr = (λ x => expr)
     | (expr expr)
     | x
     | (expr : expr)
     | (∀ (x : expr) -> expr)
     | (∃ (x : expr) expr)
     | (∃-intro expr expr)
     | (∃-elim expr expr)
     | (expr -> expr)
     | ⊥
     | (⊥-elim expr)
     | (¬ expr)
     | (expr = expr)
     | (eq-refl x)
     | (eq-elim expr expr expr expr expr)
     | true
     | false
     | (bool-ind expr expr expr expr)
     | Z
     | (S expr)
     | (nat-ind expr expr expr expr) 
     | Bool
     | Nat
     | Type

Unlike in A3Q1, you should resugar (T -> ⊥) to (¬ T) in the pretty printer.
 	 	 	 	 
To submit: A6Q3.rkt