simpa[isProper, hl] using hmem
μ : 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
U : List (Sentence L)
hU : ∀ p ∈ U, p ∈ T
d : U ⊢² [σ]
l : ProofList L
hl : l.isProper = true
hmem : List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ]) ∈ l.sequents
l' : List (Code L × List (Semiformula L ℕ 0)) :=
  (Code.wk (List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ])),
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)) ::
    l
⊢ isProper l' = true
no goals