I'm struggling to fit this into my current understanding. I guess I don't really know how incompleteness looks in a type theory setting. Terms are proofs, types are propositions. _ are theories, _ are models, _ are valid formulas?