Proofs taken from

Ben C. Moszkowski. “A Complete Axiom System for Propositional Interval Temporal Logic with Inﬁnite Time”. In: Logical Methods in Computer Science Journal 8.3 (2012). url.