no goals
α : Type u
l : List α
⊢ length (map (get l) (finRange (length l))) = length l
simp
no goals
α : Type u
l : List α
⊢ ∀ (n : ℕ) (h₁ : n < length (map (get l) (finRange (length l)))) (h₂ : n < length l),
    get (map (get l) (finRange (length l))) { val := n, isLt := h₁ } = get l { val := n, isLt := h₂ }
simp