simp only [nths, map, get]
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get (List.map Prod.fst (nths xs (n :: ns)))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }