rw [State.record_comm]
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
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₁
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₂
⊢ s₃' = record (record (Step.Exec.applied e₁) (Step.Exec.rcn e₁)) (Step.Skip.rcn e₂)
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
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₁
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₂
⊢ s₃' = record (record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)) (Step.Exec.rcn e₁)