cases m₁ <;> cases m₂ <;> simp [Member.extend] at h
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
i₁ i₂ : Component.idType Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
m₁ : Member Component.rtr i₁ rtr
m₂ : Member Component.rtr i₂ rtr
h₁ : object m₁{cpt}{j} = some o₁
h₂ : object m₂{cpt}{j} = some o₂
h : extend m₁ h₁ = extend m₂ h₂
⊢ i₁ = i₂
case root.root
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : o₁ = o₂
⊢ ⊤ = ⊤

case root.strict
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.final h₁ = StrictMember.extend a✝ h₂
⊢ ⊤ =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝

case strict.root
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₁ : object (strict a✝){cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : StrictMember.extend a✝ h₁ = StrictMember.final h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝) =
    ⊤

case strict.strict
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝¹ : ID
a✝¹ : StrictMember Component.rtr i✝¹ rtr
h₁ : object (strict a✝¹){cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.extend a✝¹ h₁ = StrictMember.extend a✝ h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝¹
    | Component.rcn => i✝¹
    | Component.val v => i✝¹) =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝