no goals
α : Type u_1
β : Type ?u.7543
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range encode
simp_rw [Set.range, Set.mem_setOf_eq, Ne.def, Option.eq_none_iff_forall_not_mem,
  Encodable.mem_decode₂, not_forall, not_not]