intro equiv
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
⊢ t ≡ t' → (Activates exec t ↔ Execution.Executable.triggers.activated exec reaction t' = true)
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ Activates exec t ↔ Execution.Executable.triggers.activated exec reaction t' = true