by_cases p x with
| isTrue hh =>
  rw [sublist_pos_tail hh]
  rw [unsublist_pos_tail hh]
  rw [ih]
| isFalse hh =>
  rw [sublist_neg_tail hh]
  rw [unsublist_neg_tail hh]
  rw [ih]
case tail
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
⊢ unsublist p (sublist p i.tail hi) = i.tail
no goals