intro Γ Δ hΓ hΔ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
⊢ (𝓓)-Consistent (Ax(𝓓), ∅)
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : ∀ p ∈ Δ, p ∈ (Ax(𝓓), ∅).2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'