case h.h
it : Iterator
n : Nat
⊢ forward it n = nextn it n
⊢ forward = nextn
funext it n
no goals
case h.h
it : Iterator
n : Nat
⊢ forward it n = nextn it n
induction n generalizing it <;> simp [forward, nextn, *]