transitivity (⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, hp⟩ : { i // p (succ i) }).val.val
case e_val.e_val.e_a
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 = i
case e_val.e_val.e_a.left
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 = ↑⟨⟨i, ⋯⟩, hp⟩.val

case e_val.e_val.e_a.right
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑⟨⟨i, ⋯⟩, hp⟩.val = i