work on hol_verification

reprove inst_aux_thm