exact ⟨Δ, Δ.prop, ⟨d⟩⟩
case intro.mk
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
b : 𝓣 ⊢ p
Δ : { Δ // ∀ π ∈ Δ, π ∈ 𝓣 }
d : ↑Δ ⊢² [p]
⊢ ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]
no goals