rw [Array.any_iff_mem_where]
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ ∃ a, a ∈ reaction.val.triggers.data ∧ Execution.Executable.triggers.activated exec reaction a = true