simp only [Option.eq_none_iff_forall_not_mem, ←not_exists]
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
⊢ rtr₁{cpt}{i} = none ↔ rtr₂{cpt}{i} = none
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
⊢ (¬∃ x, x ∈ rtr₁{cpt}{i}) ↔ ¬∃ x, x ∈ rtr₂{cpt}{i}