Unification is an operation for building a set that includes all elements of some number of sets. For example, $A \cup B \cup C$ is the set that includes all members of $A$, $B$, $C$, and no other members.
import proveit %theory
