Ugh, Coq keeps crashing on me. Apparently this proof just has too many goals. Not sure what to do about this... perhaps it's time to learn proof-by-reflection?
@akhirsch I think Adam's advice is to build a bigger machine. If you have less than 1TB of RAM, how do you even Coq?
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.