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 Ltac.
Require Import Datatypes.
Require Export Logic.
Negation of a type in Type
Properties of identity