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)
Negation of a type in Type
Properties of identity
Section identity_is_a_congruence.
Variables A B : Type.
Variable f : A -> B.
Variables x y z : A.
Lemma sym_id : identity x y -> identity y x.
Lemma trans_id : identity x y -> identity y z -> identity x z.
Lemma congr_id : identity x y -> identity (f x) (f y).
Lemma sym_not_id : notT (identity x y) -> notT (identity y x).
End identity_is_a_congruence.
Definition identity_ind_r :
forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y.
Defined.
Definition identity_rec_r :
forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y.
Defined.
Definition identity_rect_r :
forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y.
Defined.
Hint Immediate sym_id sym_not_id: core v62.