Theorem: List.Index.sublist_unsublist (GMLInit/Data/Index/Sublist.lean)

State before:
α : 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
Tactic:
rw [sublist_eq_iff_eq_unsublist]
State after:
no goals