cases h' : subTabs Y Y_in
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
⊢ Z ∈ endNodesOf ltX
case byLocalRule
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
B✝ : List TNode
next✝ : (Y : TNode) → Y ∈ B✝ → LocalTableau Y
x✝ : LocalRuleApp Y B✝
h' : subTabs Y Y_in = LocalTableau.byLocalRule x✝ next✝
⊢ Z ∈ endNodesOf ltX

case sim
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
a✝ : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim a✝
⊢ Z ∈ endNodesOf ltX