intro activates
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ Activates exec t →
    (match t' with
      | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
      | Trigger.action action =>
        Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
      | Trigger.timer timer =>
        (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
      | Trigger.startup => isStartingUp exec
      | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
      true
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
activates : Activates exec t
⊢ (match t' with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true