Theorem: Execution.State.record_comm (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
rcn₁ rcn₂ : ID
⊢ record (record s rcn₁) rcn₂ = record (record s rcn₂) rcn₁
Tactic:
simp [record]
State after:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
rcn₁ rcn₂ : ID
⊢ Set.insert rcn₂ (Set.insert rcn₁ s.progress) = Set.insert rcn₁ (Set.insert rcn₂ s.progress)

State before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
rcn₁ rcn₂ : ID
⊢ Set.insert rcn₂ (Set.insert rcn₁ s.progress) = Set.insert rcn₁ (Set.insert rcn₂ s.progress)
Tactic:
apply Set.insert_comm
State after:
no goals