have ho₂ := e₂.indep_output_eq hi.symm
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
⊢ s₁₂ = s₂₁
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
ho₂ : output s (Execution.Step.Exec.rcn e₁) = output s₂ (Execution.Step.Exec.rcn e₁)
⊢ s₁₂ = s₂₁