An Essence of SSReflect Iain Whiteside, David Aspinall, and Gudmund Grov CISA, School of Informatics University of Edinburgh Edinburgh EH8 9AB, Scotland Abstract. SSReflect is a powerful language for proving theorems in the Coq system. It has been used for some of the largest proofs in formal mathematics thus far. However, although it constructs proofs in a formal system, like most other proof lang