A tactical for applying tactics to individual proof mode hypotheses
For example, so that you can perform a rewrite
or simpl
in just one proof mode hypothesis.
Ssreflect also has such a tactical.
For example, so that you can perform a rewrite
or simpl
in just one proof mode hypothesis.
Ssreflect also has such a tactical.