reconsider T = {{}} as Tree ;
take T --> {} ; :: thesis: T --> {} is finite
thus T --> {} is finite ; :: thesis: verum