Work the following exercises from the chapter Tactics: More Basic Tactics:
filter_exercise is marked as challenging. It is, but it is
quite doable. The
forall_exists_challenge will be your first time
verifying a function you write. Pay attention to the structure of the
problem as well as the proofs themselves.
Submit your Project 3 proofs and definitions via blackboard. It is important that you use the theorem names as defined in the text. Feel free to add and prove any lemmas you feel are useful, but keep the names of the theorems in order and the same.