constructor
μ : Type ?u.1169140
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, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true) ↔
    ∃ e,
      Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
        true
case mp
μ : Type ?u.1169140
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, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true) →
    ∃ e,
      Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
        true

case mpr
μ : Type ?u.1169140
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
⊢ (∃ e,
      Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
        true) →
    ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true