bool the carrier of A is finite ;
hence _bool A is finite by Th17; :: thesis: verum