Library illtypebug

Inductive single:Type:=
|single_intro: single.

Definition singlet (A:Type):=exists! s:A, True.

Lemma uniquesingle: singlet single.

Theorem uniquesareequal: forall (A:Type),
singlet A -> forall (x y:A), x=y.

Definition identidad (A:Type) (t:A) (x:A):=x.

Theorem ill: forall (A:Type)
(t:A) (u:(A->A)) (f:A->A) (x:A),
identidad A t (f x) = (identidad (A->A) u f) x.

Theorem ident: forall (A:Type) (t:A) (x:A),
identidad A t (id x)=x.

Theorem uniq: forall (A:Type) (t:A) (x:A),
identidad A t x=x -> singlet A -> t=x.

Theorem bug: False.