First

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

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

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

Gödel's First Incompleteness Theorem