for T being full Tree
for n being Nat holds card (T -level n) = 2 to_power n