cases hc
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝¹ : Component.Valued
b✝¹ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝¹, b✝¹).1 (a✝¹, b✝¹).2
a✝ : Component.Valued
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
hc : a✝¹ = a✝
hj : b✝¹ = b✝
⊢ False
case refl
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝¹ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝, b✝¹).1 (a✝, b✝¹).2
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
hj : b✝¹ = b✝
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
⊢ False