:: deftheorem defines -tail POLNOT_1:def 38 :
for T being Polish-language
for A being Polish-arity-function of T
for n being Nat
for F being Element of Polish-expression-hierarchy (T,A,(n + 1)) holds (T,A) -tail F = T -tail F;