intro Y Y_in_ress y y_in_Y
X : TNode
ress : List TNode
rule : LocalRule X ress
⊢ ∀ Y ∈ ress, ∀ y ∈ node_to_multiset Y, ∃ x ∈ node_to_multiset X, y < x
X : TNode
ress : List TNode
rule : LocalRule X ress
Y : TNode
Y_in_ress : Y ∈ ress
y : Formula
y_in_Y : y ∈ node_to_multiset Y
⊢ ∃ x ∈ node_to_multiset X, y < x