all_goals
  simp [Trigger.lift]
  first
  | constructor
  | split <;> (constructor; assumption)
case startup
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
⊢ Trigger.lift _root_.Trigger.startup ≡ _root_.Trigger.startup

case shutdown
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
⊢ Trigger.lift _root_.Trigger.shutdown ≡ _root_.Trigger.shutdown

case port
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
⊢ Trigger.lift (_root_.Trigger.port p✝) ≡ _root_.Trigger.port p✝

case action
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
a✝ : reaction.val.actionSources.vars
⊢ Trigger.lift (_root_.Trigger.action a✝) ≡ _root_.Trigger.action a✝

case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.lift (_root_.Trigger.timer t✝) ≡ _root_.Trigger.timer t✝
no goals