# The country music theorem

In which we prove that in a universe where everyone loves either rock music or country music (or both), and there is someone who does not love rock music, there is definitely someone who loves country.

We proceed here by boldly asserting these two facts about our universe and proving the consequence.

#### About the steps

[1] In this proof we prove that `exists {x. Country x}`

without any
conditions, based on two facts about our mathematical world.

[2] The second assertion about our imagined universe.

[3] Result of rewriting all of step 1.

[4] Add a universal quantifier.

[5] This is a *consequence* of step 4, where step 4 matches the
pattern `forall {x. p x => q x}`

.

[6] This uses step 2 to conclude that the assumption
`exists {x. not (Rock x)}`

is true. It internally simplifies,
removing the `T =>`

. The statement `exists Country`

means that
the predicate `Country`

is true for someone.

[7] This is the customary way of writing an existential statement, equivalent to step 6.

#### Try it yourself

You can use this space to practice building your own proof. You might like to start by recreating the proof shown above.