. intro h Γ Δ hΓ hΔ;
  simp_all only [Set.mem_insert_iff];
  have : 𝓓 ⊬! p ⋏ (Γ.remove p).conj' ⟶ Δ.disj' := h (by
    intro q hq;
    have := by simpa using hΓ q $ List.mem_of_mem_remove hq;
    cases this with
    | inl h => simpa [h] using List.mem_remove_iff.mp hq;
    | inr h => assumption;
  ) hΔ;
  by_contra hC;
  have : 𝓓 ⊢! p ⋏ (Γ.remove p).conj' ⟶ Δ.disj' := imp_trans! andComm! $ implyLeftRemoveConj' (p := p) hC;
  contradiction;
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)
no goals