rw [List.get_map Prod.fst]
η : 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 xs { val := n.val, isLt := (_ : n.val < List.length xs) }).fst =
    List.get (List.map Prod.fst xs) { val := n.val, isLt := (_ : n.val < List.length (List.map Prod.fst xs)) }
no goals