cases u₁ <;> cases u₂
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u₁ : LawfulUpdate cpt i v rtr rtr₁
u₂ : LawfulUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
case update.update
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u✝¹ : LawfulMemUpdate cpt i v rtr rtr₁
u✝ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂

case update.notMem
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u✝ : LawfulMemUpdate cpt i v rtr rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂

case notMem.update
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₁
u✝ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂

case notMem.notMem
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝¹ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝¹ : rtr = rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂