guarded-recursion Playing with guarded recursion in Coq, based on: First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees (LICS'11) Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes (LICS'13)