Theorem: Execution.Instantaneous.Closed.rcns_perm (ReactorModel/Execution/Theorems/Grouped/Instantaneous.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
e₁ : s ↓ᵢ| s₁
e₂ : s ↓ᵢ| s₂
⊢ rcns e₁ ~ rcns e₂
Tactic:
simp [List.perm_ext_iff_of_nodup e₁.rcns_nodup e₂.rcns_nodup, e₁.mem_rcns_iff, e₂.mem_rcns_iff]
State after:
no goals