rcases Z_endOf_LR with ⟨ZS, ⟨c, c_in_C, endNodes_c_eq_ZS⟩, Z_in_ZS⟩
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
Z_endOf_LR : ∃ l, (∃ a, ∃ (h : a ∈ altLR), endNodesOf ⟨a, subTabs a ⋯⟩ = l) ∧ Z ∈ l
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
case intro.intro.intro.intro
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
ZS : List TNode
Z_in_ZS : Z ∈ ZS
c : TNode
c_in_C : c ∈ altLR
endNodes_c_eq_ZS : endNodesOf ⟨c, subTabs c ⋯⟩ = ZS
⊢ lengthOfTNode Z ≤ lengthOfTNode LR