theorem List.Vector.cons_get {α : Type u_1} {x : α} : (x ::ᵥ nil).get = ![x]

theorem LO.FirstOrder.Arith.re_iff_sigma1 {P : ℕ → Prop} : RePred P ↔ 𝚺₁-Predicate P

theorem LO.FirstOrder.Arith.goedel_first_incompleteness (T : Theory ℒₒᵣ) [𝐑₀ ≼ T] [Sigma1Sound T] [T.Delta1Definable] : ¬System.Complete T

Gödel's First Incompleteness Theorem