NNG4
NNG4 copied to clipboard
cannot apply succ_inj in succ_mul
its in the panel on the right, so my guess is it's a bug that the execution report error as "unknown identifier 'succ_inj'"
The panel could probably be improved (I think at the moment it actually lists everything that you have already unlocked?), but then you don't need that for this level anyway.
that's true, but that can also be a feature. just that you don't want to confuse the user
Same as https://github.com/leanprover-community/lean4game/issues/187