Library anomalybug

Definition Bijective (U1 U2:Type) (f:U1->U2):Prop:=
(forall a b:U1, a<>b -> f a<>f b) /\
(forall b:U2, exists a:U1, f a=b).

Definition InverseFunction (U1 U2:Type) (f:U1->U2) (g:U2->U1)
:= forall (a:U1) (b:U2), f a =b -> g b =a.

Lemma UndoInverse :
forall (U1 U2:Type) (f:U1->U2) (g:U2->U1) (a:U1),
InverseFunction U1 U2 f g -> g (f a)=a.

Theorem InverseOfBijectiveIsBijective :
forall (U1 U2:Type) (f:U1->U2) (g:U2->U1),
Bijective U1 U2 f -> InverseFunction U1 U2 f g
-> Bijective U2 U1 g.