rintro ⟨Δ, h, ⟨d⟩⟩
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
⊢ (∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]) → 𝓣 ⊢! p
case intro.intro.intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ π ∈ Δ, π ∈ 𝓣
d : Δ ⊢² [p]
⊢ 𝓣 ⊢! p