Countability of Inductive Types Formalized in the Object-Logic Level

Qinxiang Cao, Xiwei Wu

The set of integer number lists with finite length, and the set of binary trees with integer labels are both countably infinite. Many inductively defined types also have countably…