cases ltLR
LR Z : TNode
ltLR : LocalTableau LR
⊢ Z ∈ endNodesOf ⟨LR, ltLR⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
case fromRule
LR Z : TNode
C✝ : List TNode
subTabs✝ : (c : TNode) → c ∈ C✝ → LocalTableau c
ruleA✝ : LocalRuleApp LR C✝
⊢ Z ∈ endNodesOf ⟨LR, fromRule ruleA✝ subTabs✝⟩ → lengthOfTNode Z ≤ lengthOfTNode LR

case fromSimple
LR Z : TNode
isSimple✝ : Simple LR
⊢ Z ∈ endNodesOf ⟨LR, fromSimple isSimple✝⟩ → lengthOfTNode Z ≤ lengthOfTNode LR