We illustrate how to use LP by presenting some sample proofs along with explanatory comments. The proofs show how to derive some basic facts about finite sets from a simple axiomatization.

- Getting started
- Sample declarations for sorts, operators
- Sample axioms for finite sets
- Useful kinds of axioms
- Sample conjectures
- Two easy theorems
- Three theorems about union
- Alternative proofs of theorems about union
- Three theorems about subset
- An alternate induction rule
- Two final theorems about subset
- How to guide a proof