Short and informal is hard to come by here, especially by such a formal system built by such formal people.

This tutorial maybe?

https://coq.inria.fr/tutorial-nahas

This particular chapter of Software Foundations may be helpful (or it might not be. If so don't sweat it, it isn't really meant to be read in isolation)

https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...