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

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 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/ProofObjects.html https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...