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 (RC0) and the Worm Calculus (WC). Finally, it proves some basic results about RC0 and WC. The main result is the conservativity of RC0 over WC.