The Coq mailing list

[marco.servetto AT gmail.com]

Hi, I have an (I hope) very simple problem.
I need a proof that I'm inside some branch of a match case:
That is, in the following case
Definition f optA:=
  match optA with
    |Some a=>Some ( g a (p:(Some a=optA))
   |None=>None
    end.

I need to find the """p""" that have type """Some a=optA"""
any suggestion?

Thanks
Marco.