Yeah, understanding proof assistants would be the big practical thing. I can read a short proof in Lean, but a lot of it just feels like magic right now.
It looks like I was mainly missing sequent calculus (I learned all in the Hilbert style of deduction) and the convention that gamma is the whole context. I'd see the notation and wonder if I missed something. Thank you for the effort you put in on this!