Update formal.tex

compared notation for judgmental equality with that in the intro