This is a "finishing" tactic modification of simp.

• simpa [rules, ...] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

• simpa [rules, ...] will simplify the goal using rules, then try to close it using assumption.