α : Type u_1
β : Type ?u.4397
inst✝ : Encodable α
n : ℕ
a : α
⊢ (∃ a_1, decode n = some a_1 ∧ a_1 = a ∧ encode a_1 = n) ↔ decode n = some a ∧ encode a = n
α : Type u_1
β : Type ?u.4397
inst✝ : Encodable α
n : ℕ
a : α
⊢ a ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n
simp [decode₂]
no goals
α : Type u_1
β : Type ?u.4397
inst✝ : Encodable α
n : ℕ
a : α
⊢ (∃ a_1, decode n = some a_1 ∧ a_1 = a ∧ encode a_1 = n) ↔ decode n = some a ∧ encode a = n
exact ⟨fun ⟨_, h₁, rfl, h₂⟩ => ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ => ⟨_, h₁, rfl, h₂⟩⟩