rw [size_update]
C : Type ?u.18089
τ : Type ?u.18088
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
⊢ size (update cont i f) = size cont
no goals