An Example with Conjunction and Disjunction in Coq

We prove disjunction is left-distributive over conjunction in the proof assistant Coq. The same proof is explained informally in the previous video:

In the next video we prove Leibniz equality implies Coq's equality (in Coq):

[heptadecagon]

I was just wondering, how do you have emacs replace key words like forall, \/, /\, etc. with their more familiar symbols?

Thank you very much for this video!