Theorem: map_plusone_not_somezero (Saturn/PrependClause.lean)

State before:
n : Option ℕ
j : ℕ
hyp : some (j + 1) = some zero
⊢ j + 1 = zero
Tactic:
injection hyp
State after:
no goals