∃D. The constant, a, must be new to the branch [here the computer will choose for you]
∀D. Any closed term, stage 1, your choice
∀D. Any closed term, stage 2, a chosen
¬∃D.
¬∀D.
