simp [reducible_iff, Unprovable]
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
𝓢 : S
𝓣 : T
𝓤 : U
⊢ ¬𝓢 ≤ₛ 𝓣 ↔ ∃ f, 𝓢 ⊢! f ∧ 𝓣 ⊬! f
no goals