TY - RPRT TI - Inductive and Coinductive Components of Corecursive Functions in Coq AU - Yves Bertot AU - Ekaterina Komendantskaya PY - 2008 UR - https://arxiv.org/abs/0807.1524 ID - 0807.1524 ER -