let f₂ : s₂' ↓ₛ s₃' := ⟨ha₂, ht₂⟩
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃