Run a tactic in an environment with a temporarily modified reducibility attribute
for a specified declaration.
Possible reducibility attributes for a declaration:
reducible, semireducible (the default), irreducible.
Satisfy the inhabited linter
Return the attribute (as a
name) corresponding to a reducibility level.