Bijections are 1-to-1 and onto functions.
import proveit %theory # toggles between interactive and static modes
