rintro ⟨⟨Δ, h, b⟩⟩
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
⊢ Γ *⊢[𝓢]! p → ∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p
case intro.mk
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 ∈ { ctx := Γ }
b : Δ ⊢[𝓢] p
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p