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;
)
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
⊢ L ⊬! Γ.conj' ⟶ ⊥
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
⊢ L ⊬! Γ.conj' ⟶ ⊥