I didn't beat out every detail but it looks constructive to me (there is one b which should be a B). There are considerations like: Each component (in a directed graph with outdegree 1 and maximum indegree 1) is a cycle, a one way infinite directed path or a bi-infinite directed path so do a,b or c depending on the case. That is sort of excluded middle but simply shows that the constructed bijection (in this case constructed from injections A->B and B->A for the Cantor–Bernstein–Schroeder theorem) are as explicit as the ingredients but not more so (I'm not sure if that captures your question).
The well written article
Producing New Bijections from Old by Feldman D.; Propp J. in Advances in Mathematics, Volume 113, Number 1, June 1995 , pp. 1-44(0)
(available in postscript from http://faculty.uml.edu/jpropp/articles.html)
Gives a careful description of the kind of construction desired . One killer example from that paper: If P is the permutations of a set and L the linear orders of that set then there is no natural bijection from L to P (even if the set has 3 elements) because there is a distinguished permutation (the identity) but no distinguished linear order. However, there is a natural bijection from LxL to PxL using the 2 line notation.
The paper is written in a relaxed style and has a footnote indicating that Conway might not be that committed every remark and detail of the exposition.
Actually the remark that
- since 3a=3b implies a=b in finite arithmetic...for finite sets a bijection from Ax3 to Bx3 should yield one from A to B
is suspicious to me (because of the example above).
