simp [Fin.pair_succ_left]
case mk.e_a.e_val
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ ↑(i.succ.pair j) - (map (fun b => (hd, b)) L2).length = ↑(i.pair j)
no goals