have h := val_eq_of_eq h
case refl
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 }
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : 0 < count p
heq✝ : ⋯ ≅ hk✝
h : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨0, hk⟩
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
case refl
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 }
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : 0 < count p
heq✝ : ⋯ ≅ hk✝
h✝ : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨0, hk⟩
h : ↑(⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩) = ↑⟨0, hk⟩
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩