On the Coverage Property of a Derivation Compression Algorithm

We further elaborate, with a short example, on the set of compression rules and the derivation compression algorithm presented in [Haeusler et al. 2023]. We also argue a proof, done with the Lean theorem prover, that this algorithm obtains a dag-like compressed derivation from any tree-like Natural Deduction derivation in Minimal Purely Implicational Logic.