all_goals
  simp_all [actionIsPresent, portIsPresent, reactionInputs]
  try assumption
case shutdown.shutdown.a.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h : exec.state = State.shuttingDown
⊢ exec.state = State.shuttingDown
no goals