After playing around with various attempts to construct models of ZF (or IZF) in the Calculus of Inductive Constructions, I can say that CiC (even with LEM) is severely deficient compared to ZF/IZF in terms of what can be done without assuming some form of Choice. I think that Lean's banishment of these problems by just assuming Choice throughout the ecosystem might be no small part of its appeal to mathematicians.