induction xs with
| nil => contradiction
| cons x xs ih =>
  by_cases p x with
  | isTrue hx =>
    unfold unsublist
    rw [dif_pos hx]
    split
    next h =>
      rw [eqNdrec_symm] at h
      cases h
      rw [val_ndrec _ (List.sublist_pos hx).symm.symm.symm]
    next h =>
      rw [eqNdrec_symm] at h
      cases h
      rw [val_ndrec _ (List.sublist_pos hx).symm.symm.symm]
      rw [val_tail, val_tail]
      apply ih
  | isFalse hx =>
    unfold unsublist
    rw [dif_neg hx]
    rw [val_tail]
    rw [ih]
    apply congrArg
    rw [val_ndrec]
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
i : (List.sublist p xs).Index
⊢ (unsublist p i).val = i.val.val
no goals