case _ rcn₁ h₁ =>
  cases cpt
  all_goals
    intro ⟨⟩
    apply absurd hd
  case stv =>
    exact hi.no_shared_state_deps h₁ h₂ hc
  all_goals
    exact hi.left.deps_disjoint h₁ h₂ (rcn₁.target_mem_deps hc) $ by simp [Change.Normal.target]
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
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₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ ¬Change.Targets c cpt i
no goals