We use the rules to reduce a sequent to a conjunction of simple
sequents, sequents that only mentions propositional letters, with no
connectives, and no repetitions — in this example, we find a single
simple sequent, equivalent to our starting sequent in the sense that
both are valid in the same universes. This shows our starting sequent is
not a tautology. It is simple to provide a counterexample to a simple
sequent, and this provides a counter-example to the strtting sequent.