simp [getF]
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
i : ℕ
⊢ ∀ (h : 0 < length (rangeF (Nat.succ m))), getF (rangeF (Nat.succ m)) 0 h = { val := 0, isLt := (_ : 0 < Nat.succ m) }
no goals