Comment by marvinborner

T is a translation function, square brackets indicate a term within another term (its context), and braces are standard substitution. It's deliberately vague to make discovery more fun (I know this is very controversial, but the most fun papers/articles I read are the ones whose notation I don't understand at all)

I try to give just about enough information to be able to understand it given some time and experimentation.