[1] https://www.google.com/books/edition/Advanced_Topics_in_Type...
It's a coincidence, because I was just reading that chapter on pure type systems earlier today. Yes, I understand that notation. FWIW those aren't proofs; those are typing rules.
The top-left rule on page 52 says that given that:
- In context Gamma, T1 = T2 where both have kind *
- If x : T1 is added to the context Gamma, K1 = K2
you can derive that in context Gamma, (x : T1) -> K1 = (x : T2) -> K2.
A context is just a symbol table mapping names to types. Conventionally, uppercase gamma or uppercase delta is used.
The uppercase pi is just another way of writing the dependent function type. If you think of types algebraically, dependent function types are similar to repeated multiplication, which use capital pi. It's similar to how summation uses capital sigma (and therefore the dependent sum type uses capital sigma as well).
Gamma |- exp : A
This is a common pattern that says that exp has type A when the contents of Gamma are in scope.
Gamma |- exp1 = exp2 : A
This is a common pattern that says that exp1 and exp2 are equal terms of type A when the contents of Gamma are in scope.
I've found that most type system rules follow the same format more or less.
Sometimes, I do misread things. (When reading the page you linked, at first I mistook T1 = T2 for a type of kind *, then I realized I misunderstood it.)
-> is material implication, so it is an operator of the object language. |- is part of the metalanguage that you use to reason about the object language. I am not that knowledgeable in logic, however.
Frankly, I'd expect any CS student at a decent university to be able to parse that page fairly easily.