simp [sum] at h
f : Fin 0 → Nat
k : Fin (sum f)
x : (i : Fin 0) × Fin (f i)
val✝ : Nat
h : val✝ < sum f
x✝ : (i : Fin 0) × Fin (f i)
⊢ decodeSigma f ⟨val✝, h⟩ = x✝ ↔ encodeSigma f x✝ = ⟨val✝, h⟩
f : Fin 0 → Nat
k : Fin (sum f)
x : (i : Fin 0) × Fin (f i)
val✝ : Nat
h : val✝ < 0
x✝ : (i : Fin 0) × Fin (f i)
⊢ decodeSigma f ⟨val✝, h⟩ = x✝ ↔ encodeSigma f x✝ = ⟨val✝, h⟩