This reminds me slightly of Milne's interpolation theorem for classical propositional logic, which says that any proof can be re-written so that the first use of the law of the excluded middle occurs after the last use of the law of non-contradiction.