The secret is that you can convert most type B math into type A by looking at steps in a proof as rules in a term rewriting system where the terms are mathemati

The secret is that you can convert most type B math into type A by looking at steps in a proof as rules in a term rewriting system where the terms are mathematical expressions. I've not found a book that makes this point completely explicitly, but most of those which cover sequent calculus get you half way there. The rest of type B math is intuition which lets you guess at new conjectures and how to get you from the assumptions that you've made and the conjecture that you want to prove efficiently.