rfl
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
⊢ sum ((fun i => if p i then 1 else 0) ∘ succ) = sum fun i => if p i.succ then 1 else 0
no goals