case refl
α : Type u_1
l : List α
i : Fin (length l)
⊢ get l i = get l { val := i.val, isLt := (_ : i.val < length l) }
α : Type u_1
l l' : List α
h : l = l'
i : Fin (length l)
⊢ get l i = get l' { val := i.val, isLt := (_ : i.val < length l') }
cases h
no goals
case refl
α : Type u_1
l : List α
i : Fin (length l)
⊢ get l i = get l { val := i.val, isLt := (_ : i.val < length l) }
rfl