We use the rules to reduce a sequent to a conjunction of simpler sequents. In this example we find that the expression asserted by the sequent is a tautology — it is equivalent to the empty conjunction, so is valid in every universe.