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]
case cons
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
⊢ (unsublist p i).val = i.val.val
no goals