definition let p be polyhedron;
mode 0-chain of p is Element of Funcs(vertices(p),{0,1});
end;
the error with the fraenkel terms goes away. But then I have a new
problem: elsewhere in my file terms of the form
c.x
where c has type `0-chain of p' and x has type `vertex of p' (which is
defined as `Element of vertices(p)') are no longer well-formed. The
problem, I think, is that c does not have type `Function'. I suppose
one approach to this problem would be to redefine `.' for terms of
type `Element of Funcs(vertices(p),{0,1})', but that doesn't seem
appealing. What can be done?