exact i.elim0
case nil
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
i : Fin [].length
LL : List (α × β)
hLL : [] ×ˢ L2 = LL
p : Fin LL.length
hp : ↑p = ↑(i.pair j)
⊢ LL.get p = ([].get i, L2.get j)
no goals