cases ho₁ : rtr₁[.rcn][i]
case h
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
⊢ rtr₁[Component.rcn][i] = rtr₂[Component.rcn][i]
case h.none
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
ho₁ : rtr₁[Component.rcn][i] = none
⊢ none = rtr₂[Component.rcn][i]

case h.some
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
⊢ some val✝ = rtr₂[Component.rcn][i]