simp [ProvableSet, PrfSet, Provable, Classical.nonempty_pi, ←imp_iff_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
𝓢 : S
s : Set F
⊢ 𝓢 ⊢!* s ↔ Nonempty (𝓢 ⊢* s)
no goals