(* $Id$ *) Require Export Disjoint_Union. Require Export Inclusion. Require Export Inverse_Image. Require Export Lexicographic_Exponentiation. Require Export Lexicographic_Product. Require Export Transitive_Closure. Require Export Union. Require Export Well_Ordering.