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

State before:
α : Type
inst✝ : Hierarchical α
s₁✝ s₂✝¹ : State α
rcn : ID
s₁ s₂ s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
⊢ ∃ hd tl, rcns (trans a✝¹ a✝) = hd :: tl
Tactic:
simp [rcns]
State after:
no goals