subst endNodes_c_eq_ZS
case intro.intro.intro.intro
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
ZS : List TNode
Z_in_ZS : Z ∈ ZS
c : TNode
c_in_C : c ∈ a✝
endNodes_c_eq_ZS : endNodesOf ⟨c, subTabs c ⋯⟩ = ZS
⊢ lengthOfTNode Z < lengthOfTNode LR
case intro.intro.intro.intro
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
c : TNode
c_in_C : c ∈ a✝
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z < lengthOfTNode LR