. intro Γ;
  by_contra hC;
  obtain ⟨hΓs, hΓd⟩ := by simpa using hC;
  obtain ⟨U, hUc, hUs⟩ :=
    Set.subset_mem_chain_of_finite c hnc chain
      (s := ↑Γ.toFinset) (by simp)
      (by intro p hp; simp_all);
  simp [List.coe_toFinset] at hUs;
  have : (L)-Consistent U := hc hUc;
  have : ¬(L)-Consistent U := by
    simp only [ParametricConsistent, not_forall, not_not, exists_prop];
    existsi Γ;
    constructor;
    . intro p hp; exact hUs hp;
    . assumption;
  contradiction;
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥

case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c