The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

zaman.a25 AT gmail.com
 wrote:
> Thanks for your response. I dont wish to combine them. Id simply like to get
> the ProtocolEvent of p1 and then of p2, separately. So, for the last
> constructor, pick the ProtocolEvent of the first argument and return it, then
> pick the second and return it...
>   

This makes no sense to me.  You are talking about "sequencing of 
operations" within mathematics, which has no inherent concept of time 
(unlike imperative programming).

I think you need to sit down and come up with an unambiguous description 
of what you really want.  I don't believe you really know yet what 
function you want to implement, so of course implementation is challenging.