Grimm, J. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets. JFR 2010, 3, 79-126.