have image_u' : u'.image (Semiformula.lMap L.ofSubLanguage) = u := by
  ext τ; simp [u', Finset.mem_imageOfFinset_iff]
  exact ⟨by rintro ⟨a, ⟨τ, hτ, rfl⟩, rfl⟩; simp[hτ],
    by intro hτ; exact ⟨toSubLanguageFinsetSelf hτ, ⟨τ, hτ, rfl⟩, Semiformula.lMap_toSubLanguageFinsetSelf hτ⟩⟩
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
⊢ T ⊢! σ
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
⊢ T ⊢! σ