calc
  lengthOfTNode Z ≤ lengthOfTNode c := endNodesOfLEQ Z_in_ZS
  _ < lengthOfTNode LR := this
case intro.intro.intro.intro.a
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
this : lengthOfTNode c < lengthOfTNode (LR.1, LR.2)
⊢ lengthOfTNode Z < lengthOfTNode LR
no goals