this is fascinating! Thank you so much! I had no idea that the logic for Coq was more expressive, I can understand quite clearly how that can lead to breakdow

this is fascinating! Thank you so much! I had no idea that the logic for Coq was more expressive, I can understand quite clearly how that can lead to breakdowns. I'm just slowly returning to this stuff through haskell. Heady stuff, that second mailing list post.