contradiction
case nil
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
i : [].Index
hi : p i.val
j : (List.sublist p []).Index
⊢ sublist p i hi = j ↔ i = unsublist p j
no goals