Comment by Sniffnoy

Ah, I missed that, thanks. That said, I think there's still a big difference between "only omits a finite number of hypergraphs" and "only omits a finite number of hypergraphs of bounded size". I'd regard the latter as nearly a complete proof, not so much the former. (E.g., I don't think anyone would say that we have a nearly complete proof of Artin's primitive root conjecture.) Now, it sounds like this is the latter in the sense that it can be made so, but it also sounds like it's not explicitly the latter and someone needs to actually still do that work.