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