rintro rfl
case some
α : Type u_1
inst✝ : Encodable α
e i : ℕ
val✝ : α
⊢ encode val✝ = i → ∃ a, decode i = some a
case some
α : Type u_1
inst✝ : Encodable α
e : ℕ
val✝ : α
⊢ ∃ a, decode (encode val✝) = some a