generalize hLL : L1 ×ˢ L2 = LL at p
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin L1.length
j : Fin L2.length
p : Fin (L1 ×ˢ L2).length
hp : ↑p = ↑(i.pair j)
⊢ (L1 ×ˢ L2).get p = (L1.get i, L2.get j)
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin L1.length
j : Fin L2.length
LL : List (α × β)
hLL : L1 ×ˢ L2 = LL
p : Fin LL.length
hp : ↑p = ↑(i.pair j)
⊢ LL.get p = (L1.get i, L2.get j)