[mizar] unused loci again

[Jesse Alama <alama@stanford.edu>]

I'd like the term {} to have the type `Element of bool X', for every set
X.  How might one express this in mizar?  Registrations apparently won't
do:

  registration
    let X be set;
    cluster
      {} -> Element of bool X;
  ::>                     *100
    coherence;
  end;

Nor can I redefine the term:

  definition
    let X be set;
    redefine func {} -> Element of bool X;
  ::>              *100
    coherence;
  end;

I'm aware of ways to get around this, such as explicitly typing the term
as "{}(X)".  Another approach is to give a name to the empty set with
a statement like

  reconsider emptyset = {} as Element of bool X by sometheorem;

But, if possible, I'd like to stick with the syntatically nice approach
of using just the bare "{}".  Any ideas?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)