Port reusable theory from the ESPADA proof

[andres-erbsen]

If you like, you can remove the entire ESPADA directory. I don't plan to maintain this proof. If you do this, create a ticket (assigned to me) reminding me to look through this proof and see if there is any useful theory that should be extracted. @adampetcher