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

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
⊢ (∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! p ⋏ Γ.conj' ⟶ Δ.disj') →
    (𝓓)-Consistent (insert p T, U)
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
⊢ (∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! p ⋏ Γ.conj' ⟶ Δ.disj') →
    (𝓓)-Consistent (insert p T, U)