J. Grimm, “Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets”, JFR, vol. 3, no. 1, pp. 79–126, Jan. 2010.