exact Complete.complete (h f)
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
M : Type u_3
inst✝¹ : Semantics F M
𝓢 : S
𝓜 : M
inst✝ : Complete 𝓢 𝓜
h : ∀ (f : F), 𝓜 ⊧ f
f : F
⊢ 𝓢 ⊢! f
no goals