have := u₁'.obj?_preserved (.inr hi₂) ▸ u₂'.obj?_preserved (.inr hi₁)
case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
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₂✝
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₂
hi₁ : ¬i = i₁
hi₂ : ¬i = i₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
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₂✝
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₂
hi₁ : ¬i = i₁
hi₂ : ¬i = i₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝