intro q hq
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! p ⋏ Γ.conj' ⟶ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 = p ∨ p_1 ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
⊢ ∀ p_1 ∈ List.remove p Γ, p_1 ∈ T
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! p ⋏ Γ.conj' ⟶ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 = p ∨ p_1 ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
q : Formula α
hq : q ∈ List.remove p Γ
⊢ q ∈ T