intro t ns i hi
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (ns : List (Fin (ncols t))) (i : Nat) (hi : i < List.length ns),
    List.get (header (selectColumns2 t ns)) { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
      List.get (header t) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (header (selectColumns2 t ns)) { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (header t) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))