finish [apply], [symmetry], [rev_exercise1], explain difference between [apply] and [rewrite], read final list of tactics