@[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.InferenceSystem.derivation Cslib.Logic.InferenceSystem.Default Γ // Cslib.Logic.CLL.Proof.cutFree q = true }