 Another interesting case study is found in Colyvan et al. 2018. There the main example is the theorem to the effect that, given any set X, there exists a free group over X (The Free Group Theorem). The authors analyze and contrast a constructive proof of the result and a more abstract but non-constructive proof. They compare and contrast the two proofs with known models of scientific explanation and find that the first proof has features in common with the reductive account of explanation while the second is more in line with unificationist accounts. They conclude that both proofs have explanatory virtues. The discussion ends up highlighting the problem of how to compare and rank the explanatoriness of proofs and claims that explanatory virtues come in degrees. An additional case study concerning compactness is provided in Paseau 2010. 