all_goals
  simp_all [actionIsPresent, portIsPresent, reactionInputs]
  try assumption
case shutdown.shutdown.shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
a✝ : exec.state = State.shuttingDown
⊢ (match Trigger.shutdown 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
no goals