split at h
case succ.mp
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 :
  (if h : p 0 then
      match ↑k, ⋯ with
      | 0, hk => ⟨0, ⋯⟩
      | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩
    else ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
⊢ encodeSubtype p i = k
case succ.mp.isTrue
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✝ : p 0
h :
  (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
⊢ encodeSubtype p i = k

case succ.mp.isFalse
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✝ : ¬p 0
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
⊢ encodeSubtype p i = k