have : 𝓓 ⊬! (p :: Γ).conj' ⟶ Δ.disj' := h (by simp; intro q hq; right; exact hΓ q hq;) hΔ
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
h : (𝓓)-Consistent (insert p T, U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! p ⋏ Γ.conj' ⟶ Δ.disj'
⊢ False
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
h : (𝓓)-Consistent (insert p T, U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! p ⋏ Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊬! (p :: Γ).conj' ⟶ Δ.disj'
⊢ False