Theorem: LO.System.incomplete_iff_exists_undecidable (Logic/Logic/System.lean)

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝³ : System F S
inst✝² : System F T
inst✝¹ : System F U
inst✝ : LogicalConnective F
𝓢 : S
⊢ ¬Complete 𝓢 ↔ ∃ f, Undecidable 𝓢 f
Tactic:
simp [Complete, Undecidable, not_or]
State after:
no goals