split at hc <;> try contradiction
α : 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
hc :
  c ∈
    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
⊢ ¬Change.Targets c cpt i
case h_1
α : 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
x✝ : Component.type α Component.rcn
heq✝ : s.rtr[Component.rcn][i₁] = some x✝
hc : c ∈ (fun x => x.body (input s i₁)) x✝
⊢ ¬Change.Targets c cpt i