subst el
c n : ℕ
H : SearchUpTo c n
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)
c n : ℕ
H : SearchUpTo c n
H' : c = sumOfSquares (digits 10 n) → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)