B. Barras, “Sets in Coq, Coq in Sets”, JFR, vol. 3, no. 1, pp. 29–48, Jan. 2010.