Dear Andrzej, >I think that with the de Bruijn factor acceptable, we >should be more and more concerned with the comfort of >formalization. For me, being able to have types that faithfully model concepts that might (for some of the parameters) be empty, would add a lot of comfort to Mizar. Freek