exact hi.left.deps_disjoint h₁ h₂ (rcn₁.target_mem_deps hc) $ by simp [Change.Normal.target]
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.act, id := i } ∉ rcn₂.deps Kind.in
no goals