learn about [apply_with]. do trans_eq examples and exercises. TODO: why does the tactic need me to prove eq1 and eq2 if it matches trans_eq exactly?