@[reducible, inline]

abbrev Cslib.Logic.CLL.CutFreeProof {Atom : Type u_1} (Γ : Sequent Atom) : Type u_1

A CutFreeProof is a Proof without cuts (applications of Proof.cut).

Equations

• Cslib.Logic.CLL.CutFreeProof Γ = { q : ⇓Γ // Cslib.Logic.CLL.Proof.cutFree q = true }