apply List.zip_length_eq_of_length_eq _ _ h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : List.length t₁.rows = List.length t₂.rows
⊢ List.length (List.zip t₁.rows t₂.rows) = List.length t₁.rows
no goals