simp_all
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
no goals