# Worms in Coq

This library defines the language of closed strictly positive formulas and of
worms. Then it defines the closed fragment of the Reflection Calculus
(RC^{0}) and the Worm Calculus (WC). Finally, it proves some basic
results about RC^{0} and WC. The main result is the conservativity of
RC^{0} over WC.