theorem Th8: :: ABCMIZ_A:8

Vars misses Constructors