intro
case zero.mp
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
⊢ decodePi f k = x → encodePi f x = k
case zero.mp
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
a✝ : decodePi f k = x
⊢ encodePi f x = k