:: deftheorem ARGS defines args ABCMIZ_A:def 10 :
for S being non empty non void ManySortedSign
for X being empty-yielding ManySortedSet of the carrier of S
for e being Element of (Free (S,X))
for b₄ being DTree-yielding FinSequence holds
( b₄ = args e iff e = (e . {}) -tree b₄ );