have he := Equivalent.obj?_rcn_eq e.equiv
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
⊢ (match s₁.rtr[Component.rcn][i], [], fun x => x.body (input s₁ i) with
    | some x, x_1, f => f x
    | none, y, x => y) =
    match s₂.rtr[Component.rcn][i], [], fun x => x.body (input s₂ i) with
    | some x, x_1, f => f x
    | none, y, x => y
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
he : s₁.rtr[Component.rcn] = s₂.rtr[Component.rcn]
⊢ (match s₁.rtr[Component.rcn][i], [], fun x => x.body (input s₁ i) with
    | some x, x_1, f => f x
    | none, y, x => y) =
    match s₂.rtr[Component.rcn][i], [], fun x => x.body (input s₂ i) with
    | some x, x_1, f => f x
    | none, y, x => y