cases j
case mk
α : Type u_1
L1 L2 : List α
j : Fin L2.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
⊢ L1 = L2 → ↑⟨val✝, isLt✝⟩ = ↑j → L1.get ⟨val✝, isLt✝⟩ = L2.get j
case mk.mk
α : Type u_1
L1 L2 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L2.length
⊢ L1 = L2 → ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩ → L1.get ⟨val✝¹, isLt✝¹⟩ = L2.get ⟨val✝, isLt✝⟩