constructor
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction ↔
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true
case mp
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction →
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true

case mpr
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true →
    Triggers exec reaction