simp only [unsublist]
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
⊢ unsublist p (⋯ ▸ i.tail) = (unsublist p i).tail
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
⊢ (if h_1 : p x then
      match ⋯ ▸ ⋯ ▸ i.tail with
      | head => head
      | i.tail => (unsublist p i).tail
    else (unsublist p (⋯ ▸ ⋯ ▸ i.tail)).tail) =
    (unsublist p i).tail