Require Prelude.
Require Logic_Type.
Require Logic_TypeSyntax.
Require Equality.