pub type Eq<T, U> = And<Imply<T, U>, Imply<U, T>>;
Logical EQ.
The output type for commuted product.
Commutes product.
Creates a product out of two propositions.