. intro h Γ hΓ;
  have := @h (Γ.remove p) (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;
  );
  by_contra hC;
  have := imp_trans! andComm! $ implyLeftRemoveConj' (p := p) hC;
  contradiction;
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
no goals