simp [e.indep_input_eq hi h $ he ▸ h]
case some
α : 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]
val✝ : Component.type α Component.rcn
h : s₁.rtr[Component.rcn][i] = some val✝
⊢ val✝.body (input s₁ i) = val✝.body (input s₂ i)
no goals