rw [sublist_pos_head]
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x✝ : α
xs✝ : List α
hi : p head.val
⊢ unsublist p (sublist p head hi) = head
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x✝ : α
xs✝ : List α
hi : p head.val
⊢ unsublist p (⋯ ▸ head) = head