have e₂ := Equivalent.trans u₁'.equiv u₂'.equiv
α : 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₂
⊢ rtr₂ = rtr₂'
α : 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₂'
⊢ rtr₂ = rtr₂'