elim_casts
case e_a.e_i
α : 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
⊢ ⋯ ▸ ⋯ ▸ i = i
no goals