Proof formats for SAT solvers have diversified over the last decade, enabling new features such as extended resolution-like capabilities, very general extension-free rules, inclusion of proof hints, and pseudo-boolean reasoning. Interference-based methods have been proven effective, and some theoretical work has been undertaken to better explain their limits and semantics. In this work, we combine the subsumption redundancy notion from [Buss, Thapen '19] and the overwrite logic framework from [Rebola-Pardo, Suda '18]. Natural generalizations then become apparent, enabling even shorter proofs of the pigeonhole principle (compared to those from [Heule, Kiesl, Biere '17]) and smaller unsatisfiable core generation.