rw [sublist_eq_iff_eq_unsublist]
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
i : (List.sublist p xs).Index
hi : p (unsublist p i).val
⊢ sublist p (unsublist p i) hi = i
no goals