simp only [nrows, crossJoin, List.length_map, Schema.length_eq_List_length]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
⊢ nrows (crossJoin t₁ t₂) = nrows t₁ * nrows t₂
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
⊢ List.length (List.prod t₁.rows t₂.rows) = List.length t₁.rows * List.length t₂.rows