cases cpt <;> try cases i'
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
cpt : Component
i' : Component.idType cpt
o : Component.type (Component.type α Component.rtr) cpt
h : rtr{Component.rtr}{i} = some rtr'
ho : rtr'[cpt][i'] = some o
⊢ ∃ j, rtr[cpt][j] = some o
case val
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
v✝ : Component.Valued
i' : Component.idType (Component.val v✝)
o : Component.type (Component.type α Component.rtr) (Component.val v✝)
ho : rtr'[Component.val v✝][i'] = some o
⊢ ∃ j, rtr[Component.val v✝][j] = some o

case rtr.none
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

case rtr.some
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
val✝ : ID
ho : rtr'[Component.rtr][some val✝] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

case rcn
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
i' : Component.idType Component.rcn
o : Component.type (Component.type α Component.rtr) Component.rcn
ho : rtr'[Component.rcn][i'] = some o
⊢ ∃ j, rtr[Component.rcn][j] = some o