You don't sound like you've heard of the Curry-Howard isomorphism. We want practical dependently typed programming languages, ZFC is useless for that. Furthermore, LEM is never denied, it's just not adopted as an axion and thus requires proof per case.