rw [State.record_comm]
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record s₂' (Step.Skip.rcn f₂) = record (Step.Exec.applied e₂) (Step.Exec.rcn e₂)
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record (record z₂ (Step.Skip.rcn f₂)) (Step.Exec.rcn e₂) = record (Step.Exec.applied e₂) (Step.Exec.rcn e₂)