case a
α : Type u_1
β : Type ?u.7117
inst✝ : Encodable α
a a✝ : α
⊢ a✝ ∈ decode₂ α (encode a) ↔ a✝ ∈ some a
α : Type u_1
β : Type ?u.7117
inst✝ : Encodable α
a : α
⊢ decode₂ α (encode a) = some a
ext
no goals
case a
α : Type u_1
β : Type ?u.7117
inst✝ : Encodable α
a a✝ : α
⊢ a✝ ∈ decode₂ α (encode a) ↔ a✝ ∈ some a
simp [mem_decode₂, eq_comm, decode₂_eq_some]