This is a "finishing" tactic modification of
simp. It has two forms.
simpa [rules, ...] using ewill simplify the goal and the type of
rules, then try to close the goal using
Simplifying the type of
emakes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.
simpa [rules, ...]will simplify the goal and the type of a hypothesis
thisif present in the context, then try to close the goal using the