The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Hi,
I have another problem with  match-returns.
This time I can provide a very minimal working example.
Can someone help me in the proof of the last theorem? (nat and bool
are the standard ones)
Thanks a lot.
Marco.

Definition f (x:nat):= true. (*some complex calculation I do not want
to unfold ever*)
Record R:= r{
data:nat;
cond: true=f data
}.
Definition rK (n:nat):=
let res:=f n in
(match res as x return x=res->_ with
  | true => fun p=> Some (r n p)
  | false =>fun p=> None
 end)(refl_equal res).
Theorem rKFix:
forall(n: nat)(myR:R),
Some myR=rK n->data myR=n.
Proof.
?????