cases b <;> simp[ofDerivation, sequents]
case mk
μ : Type ?u.778856
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 μ
Γ : Sequent L
b :  ⊢¹ Γ
hb : CutFree b
⊢ Γ ∈ (ofDerivation ⟨b, hb⟩).sequents
case mk.cut
μ : Type ?u.778856
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 μ
Γ : Sequent L
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Γ)
a✝ : Derivation (~p✝ :: Γ)
hb : CutFree (a✝¹.cut a✝)
⊢ ∃ a, (a, Γ) ∈ ofDerivation ⟨a✝¹.cut a✝, hb⟩