have ht₁ := e₁.indep_triggers_iff h.symm |>.mpr e₂.triggers_rcn
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec 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₁ (rcn (exec e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃