[POPLmark] how to believe a twelf proof

[Randy Pollack]

Bob and Karl,

A possibly trivial question about your note.  On p. 3 it says "Rather
than specify base types, we will instead consider types with free type
variables."  (I suppose "types" here means "object language types".)
The Twelf signature immediately below does specify a base type

  o : type.

I suppose there could still be free type variables, but on p. 4 the
world for adequacy of the representation of types is given as empty.
Doesn't that mean no free type variables?

Randy