Def PM{i} == q:Type proto_sigma:Type proto_pi:Type(Void+proto_pi)(q(proto_sigma+proto_pi)q(proto_sigma+proto_pi))qqq

Thm* PM{i} Type{i'}