simp [Complete, Undecidable, not_or]
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
no goals