@Seanny123 for fig 5 you incl maybe tightly connected to fig 4 they cite these papers, try looking into them... yes they do not seem to really explain the diagram(s) and make major assumptions about notation held in prior papers. [Chlipala et al. 2005; Christiansen 2013; Dunfield and Krishnaswami 2013; Pierce and Turner 2000] are you interested in implementing some of their ideas?

the diagrams look close to/ or variant of sequent calculus en.wikipedia.org/wiki/Sequent_calculus