cases h
case mk.mk
α : Type u_1
L1 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
h : val✝¹ = val✝
⊢ L1.get ⟨val✝¹, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩
case mk.mk.refl
α : Type u_1
L1 : List α
val✝ : ℕ
isLt✝¹ isLt✝ : val✝ < L1.length
⊢ L1.get ⟨val✝, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩