The Coq mailing list

[Simao Desousa <Simao.Desousa AT sophia.inria.fr>]

Hello,

Let me explain my problem with a dummy example:
Given two sets A and B, I state, by an hypothesis, 
that I have a function f from A to (Exc B).
I define a function g by case analysis upon the result of f.


Definition g:=[x:A] Cases (f x) of
                     (value  u) => ....
                   |  _ => ....
                  end.

For proving properties of g by case analysis, 
I destruct it using the "Case" tactic, and this leads 
me at some stage to prove  (f x) = (value u) while I am 
in the first case of the analysis.
Unfortunately Case doesn't create as hypothesis this equality.

How can I remind to coq this fact?
One solution may be to state an extra hypothesis
(x:A)(u:B){(f x)=(value u)}+{(f x)=Error},
 and redefine g using it, but I would like to avoid it.


thanks, 

Simao Sousa