assumption
case timer.timer.a.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : reaction.val.timers
h : (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ t✝)).isFiring = true
⊢ (Executable.timer exec { reactor := a✝, timer := (_ : reaction.val.timers = timers (Path.class a✝)) ▸ t✝ }).isFiring =
    true
no goals