The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Jevgenijs,

  The error comes from a bug of "simpl" which performs unexpected
eta-reductions even though the eta-rule is not part of the definition
of the Calculus of Inductive Constructions.

  Due to this bug, your proof requires eta-conversion and is then
indeed not type-checkable in the CIC.

  Change your definition of Equal e.g. to

Definition Equal:=(fun (X:CSetoid)=>cs_eq (c:=X) : X->X->CProp).

  and all will go well.

  On our side, we'll fix the bug of "simpl" (typically, in your case,
the result of "simpl" on "B_Cases0 x2 a b" should have been "B_Cases
(fun x y : bool => BEqual x y) x2 a b" and not "B_Cases BEqual x2 a b"
-- compare with the result of "compute").

  Best regards,

  Hugo Herbelin

PS: please rather use coq-bugs 
(coq-bugs AT coq.inria.fr
 or
http://coq.inria.fr/bin/coq-bugs) to send bug reports.