rintro ⟨Δ, h, ⟨d⟩⟩
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
⊢ (∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p) → Γ *⊢[𝓢]! p
case intro.intro.intro
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
Δ : List F
h : ∀ q ∈ Δ, q ∈ Γ
d : { ctx := Δ } ⊢ p
⊢ Γ *⊢[𝓢]! p