use this
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
this : { x // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }
⊢ ∃ Y, ∃ (h : Y ∈ a✝), E ∈ endNodesOf (subTabs Y h)
case h
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
this : { x // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }
⊢ ∃ (h : ↑this ∈ a✝), E ∈ endNodesOf (subTabs (↑this) h)