simp_all [Reaction.Mutates]
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ Reaction.Normal rcn₂
no goals