induction s₁ generalizing rtr₂ <;> cases s₂
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
⊢ s₁ ∼ s₂
case final.final
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝¹ : Component.type α cpt
a✝¹ : rtr✝{cpt}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α cpt
a✝ : rtr₂{cpt}{i} = some o✝
⊢ final a✝¹ ∼ final a✝

case final.nested
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝ : Component.type α cpt
a✝² : rtr✝{cpt}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember cpt i rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ final a✝² ∼ nested a✝ a✝¹

case nested.final
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember cpt i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), a✝¹ ∼ s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α cpt
a✝ : rtr₂{cpt}{i} = some o✝
⊢ nested a✝² a✝¹ ∼ final a✝

case nested.nested
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember cpt i rtr₂✝¹
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), a✝² ∼ s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember cpt i rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ nested a✝³ a✝² ∼ nested a✝ a✝¹