first
| constructor
| split <;> (constructor; assumption)
case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.timer { reactor := reactor, timer := (_ : reaction.val.timers = timers (Path.class reactor)) ▸ t✝ } ≡
    _root_.Trigger.timer t✝
no goals