You could have one really hard to understand proof of a theorem and then a lot of interesting human-understandable stuff that relies on that theorem. We already have lots of proofs with oracles, where you can work out consequences of what kind of structures and solutions could exist if you had some magic thing to solve a hard part, so it just seems like a variation on that. Many people learn calculus or even the real numbers without understanding the complete formalization from set theory.