for T being full Tree
for n being non zero Nat holds len (FinSeqLevel (n,T)) = 2 to_power n