Unfolds the assertion.
This is an opaque wrapper around
Nat.pow to prevent lean from unfolding the definition of
Nat.pow on numerals. The arbitrary precondition
p is actually a formula of the form
Nat.pow a' b' = c' but we usually don't care to unfold this proposition so we just carry a
reference to it.
This is the key to making the proof proceed as a balanced tree of applications instead of a linear sequence. It is just modus ponens after unwrapping the definitions.