On Sat, Apr 20, 2013 at 6:06 AM, Daniel Peebles <pumpkingod at gmail.com> wrote: > You can't prove them equal in Agda, and you probably shouldn't be able to in > Coq either (it breaks subject reduction) but you can anyway. Are you sure you can prove them *equal* in Coq? Chlipala only proves that they are bisimilar. Paolo