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
case h_2
α : 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
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    i.val.val
no goals