Library Coq.Init.Logic_Type
This module defines type constructors for types in Type
(Datatypes.v and Logic.v defined them for types in Set)
Set Implicit Arguments.
Require Import Datatypes.
Require Export Logic.
Negation of a type in Type
Properties of identity