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.
This rather unintuitive case came up in the Discord.
Consider this solution to Power World Level 2:
This finishes the proof despite not seeming to handle the inductive case. This is (I think) because
rwahasn't been modified, which means it callsreflafter performing the rewrites. Then, theassumptioninrwais able to solve the inductive case, since we haveAs
0^succ k = 0^k * 0 = 0by definitional equality, as well as0 ^ succ (succ k) = 0also being true by defeq, this means that both the goal andhreduce to0 = 0, andassumptionfinds this and closes the inductive case.As a side note, through all the definitional equalities, this level can be solved by just
refl.