b.ll41 cleanup:
* removed outer "proof" thanks to built-in \subseteq inference rule
* removed some unnecessary "let"s
* used "tl" instead of "drop 1"
* used fewer assumptions in some proof steps
* "hence" → "then have", "thus" → "then show" (I can point you to Makarius' justification for this)
* explicit reference to assumptions
* split some &'s into meta-language "and", so that separate facts can be referred to