feat(tactic/congrm + test/congrm): partially fix a parsing issue

[adomani]

This PR tries to fix this issue raised by Heather. However, it only fixes the further minimized issue.

I added the solved issue as a test, but am stumped on solving the full issue.

E.g., can you get both of the following examples to work?

import tactic.congrm

--  works
example {a : Prop} :
  (∃ k : Prop, a) ↔ ∃ k : Prop, a :=
by congrm (∃ k, _); refl

--  fails
example {a : Prop} :
  (∃ k : Prop, a) ↔ ∃ k : Prop, a :=
by congrm ∃ k, _; refl

---