I don't know if this is the correct place for this, but I was reading this:
and I don't fully understand how they are forming these proofs. For example, I was trying to follow Proof of (Tb5) (towards the top of p. 69) but I don't fully understand how they are making the jumps that they do. Maybe I don't understand the process of doing these proofs, but I can't really find anything with a better description online.
I tried working through the "trivial" proof of (Tb8) on the bottom of p. 69, but I don't know where to go after writing the definition of atnext.
Can someone explain to me what is going on in plain English? Any suggestions on reading to understand proofs like this?