Library types

Require Export types_base.
Require Export JMeqmaptype.


Lemma formulae_typeeq: forall (A:Type) (B:Type),
A=B -> ((A->Prop)=(B->Prop)).
Implicit Arguments formulae_typeeq [A B].


Lemma function_typeeq: forall (A B C:Type),
A=B -> ((A->C)=(B->C)).
Implicit Arguments function_typeeq [A B].

Lemma match_boolunique: forall (A:Type) (x:A) (b:bool),
match b with
|true=>x
|false=>x
end=x.
Print match_boolunique.


Lemma nat_destruct: forall n:nat, {p|n=S p}+{n=0}.

Definition injective (A B:Type) (f:A->B):Prop:=
(forall a b:A, f a=f b->a=b).
Implicit Arguments injective [A B].

Theorem id_injective: forall (A:Type), injective (@id A).

Lemma exists_injective: forall (A:Type), exists f:A->A,
injective f.

Theorem eq_injective: forall (A B:Type), A=B->
exists f:A->B, injective f.

Lemma composition_injective: forall (A B C:Type)
(f:B->C) (g:A->B), injective f->injective g->
injective (f o g).