Mark things as irreducible?

[shingtaklam1324]

This rather unintuitive case came up in the Discord.

Consider this solution to Power World Level 2:

induction m with k h,
rwa [pow_succ, mul_zero],

This finishes the proof despite not seeming to handle the inductive case. This is (I think) because rwa hasn't been modified, which means it calls refl after performing the rewrites. Then, the assumption in rwa is able to solve the inductive case, since we have

h : 0 ^ succ k = 0
⊢ 0 ^ succ (succ k) = 0

As 0^succ k = 0^k * 0 = 0 by definitional equality, as well as 0 ^ succ (succ k) = 0 also being true by defeq, this means that both the goal and h reduce to 0 = 0, and assumption finds this and closes the inductive case.

As a side note, through all the definitional equalities, this level can be solved by just refl.