% The cardinality of a set. The |X| notation conflicts with the
% absolute value, and the meaning of card(X) is clear at once, so we
% The cardinality of a set. The |X| notation conflicts with the
% absolute value, and the meaning of card(X) is clear at once, so we