Hint: search "add", or watch this tutorial.

ProofCloud is a proof search engine for verified proofs debuted from INRIA as a platform for the representation of proof checking and proof analysis results.
There are six packages from OpenTheory so far. A short description of ProofCloud and Holide2 is here. The paper of ProofCloud and Holide2 is here. In addition, a hacking mannual of OpenTheory is available here.

Need some help?