Logical System default ∃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, the constant 'a' chosen ¬∃D. ¬∀D. Tree Predicate Exercises: Roll your own Book traversal links for Review of Tree Predicate Rules ‹ Tree Tutorial 4: Predicate Logic Trees Up Tree Predicate Exercises: Roll your own ›