exact Eq.symm h
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
h : List.length vs = List.length t.rows
⊢ List.length t.rows = List.length vs
no goals