The contraction rule (c) (discussed also in this blog post) is a familiar obstacle to anyone aiming to use the sequent calculus to establish a property of the underlying logic. Simply stated the issue is that the premise of the rule is more complicated (contains more content) than its conclusion, and hence proof…
