The Coq mailing list

[rcp AT Cs.Nott.AC.UK]

That should be:

How can I prove the following two functions are the same (if at all)?

Lemma id_fin_fun: (fun (n:nat) (i: Fin n) => i) = (fun (n:nat) (i:Fin n) 
=> rv n (rv n i).

Where rv (n:nat) : Fin n -> Fin n, and reverses the order of Fin n. There 
is a proof: forall (n:nat) (i: Fin n), rv n (rv n i) = i. When I use 
extensionality I get an error - "unbounded reference in environment".


Thanks,

RP.

 



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.