simp at Z_endOf_LR
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
Z_endOf_LR : Z ∈ endNodesOf ⟨LR, fromRule lrApp subTabs⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
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