Important properties of setof

Holmes uses a Schroeder-Bernstein construction to get a bijection from the universe onto the set of characteristic functions. The starting point of such a construction is an injection from the universe into the set of all characteristic functions. The next two clauses say that setof is such a one-to-one function into the set of all characteristic functions.
list(usable).
a(charq,a(setof,x)) = p1.
end_of_list.

Proof that setof x is a characteristic function | OTTER output file


list(usable).
a(setof,x) != a(setof,y) | x = y.
end_of_list.

Proof that setof is one-to-one | OTTER output file


up show outline