update do_app_exh proof

the opapp part isn't included since that moved to a separate function.
also this proof can probably be sped up if desired (every_case_tac is
slow).
add missing catchall cases to do_opapp_i2 and do_opapp_exh