. contrapose; push_neg; apply iff_ParametricConsistent_insert₂.mp;
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)
no goals