Add more isomorphisms

Specifically:
 * Congruence over products and sums
 * Congruence over Maybe
 * Demonstrate isos of Maybe using sum and unit isos
 * Distributivity of products over sums
 * Maybe (Fin n) iso Fin (S n)
 * Fin 0 iso _|_
 * Either (Fin n) (Fin m) iso Fin (n + m)
 * (Fin n, Fin m) iso Fin (n * m)