failed proof attempt for exh_to_exists_match

probably need to do an induction on how many tags come out of the call
to get_tags, but it's difficult to set up the general statement for
induction in the current setup; have to think about what it should be.