Theorem: Execution.Instantaneous.Step.TC.rcns_trans_eq_cons (ReactorModel/Execution/Theorems/Grouped/Instantaneous.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s : State α
e₁ : s ↓ᵢ s₁
e₂ : s₁ ↓ᵢ+ s₂
⊢ rcns (trans e₁ e₂) = Execution.Instantaneous.Step.rcn e₁ :: rcns e₂
Tactic:
simp [rcns, Step.rcn]
State after:
no goals