Zählbarkeit induktiver Typen, formalisiert in der Objektlogikebene