intro Z_endOf_Y
LR Z : TNode
LR_simp : Simple LR
⊢ Z ∈ endNodesOf ⟨LR, fromSimple LR_simp⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
LR Z : TNode
LR_simp : Simple LR
Z_endOf_Y : Z ∈ endNodesOf ⟨LR, fromSimple LR_simp⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR