:: deftheorem defines is_a_prefix_of TREES_1:def 1 :
for p, q being FinSequence holds
( p is_a_prefix_of q iff ex n being Nat st p = q | (Seg n) );