simp
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 : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ ∀ p_1 ∈ p :: Δ, p_1 ∈ cons p 𝓣
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 : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ ∀ a ∈ Δ, a = p ∨ a ∈ 𝓣