Theorem: Execution.Step.Skip.triggers_iff (ReactorModel/Execution/Theorems/Step/Skip.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
i : ID
e : s₁ ↓ₛ s₂
⊢ Triggers s₁ i ↔ Triggers s₂ i
Tactic:
simp [e.dst_eq, Triggers.iff_record (s := s₁) (i₁ := e.rcn)]
State after:
no goals