"Cardinalities of Finite Relations in Coq."

Paul Brunet, Damien Pous, Insa Stucke (2016)
a service of Schloss Dagstuhl - Leibniz Center for Informatics