rintro ⟨l, U, hU, hl, hproper⟩
μ : Type ?u.1107580
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
⊢ (∃ l U,
      (U.all fun x => decide (T x)) = true ∧
        List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents ∧ l.isProper = true) →
    T ⊢! σ
case intro.intro.intro.intro
μ : Type ?u.1107580
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
l : ProofList L
U : List (Sentence L)
hU : (U.all fun x => decide (T x)) = true
hl : List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents
hproper : l.isProper = true
⊢ T ⊢! σ