next heq _ =>
  match k, i with
  | ⟨_,_⟩, ⟨⟨0,_⟩, _⟩ => rfl
  | ⟨k,hk⟩, ⟨⟨i+1,hi⟩, hp⟩ =>
    cases heq
    simp only [encodeSubtype, dif_pos h0] at h
    have h := val_eq_of_eq h
    rw [val_ndrec] at h
    contradiction
case h_1
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h : encodeSubtype p i = k
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
⊢ ⟨0, ⋯⟩ = i

case h_2
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h : encodeSubtype p i = k
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝¹ : Nat
hk✝¹ : k✝¹ < count p
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq✝¹ : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
case h_2
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h : encodeSubtype p i = k
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝¹ : Nat
hk✝¹ : k✝¹ < count p
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq✝¹ : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i