intro h
case mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩ → decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
case mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h : encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩