As other people note, a lot of those seem to be local aliases defined by the author. But the most important thing to understand about Coq is that it's meant to

As other people note, a lot of those seem to be local aliases defined by the author. But the most important thing to understand about Coq is that it's meant to be read in an IDE. The IDE will show you, at each step, what has been proved and what remains to be proved. The "tactics" you see above basically mean, "At this point in the proof, we can make progress by substituting Hv. And in context, this will make sense. But without being able to see the proof state at each step, Coq can be incredibly cryptic.