exact Z_in
case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
no goals