Computing in coq with infinite algebraic data structures | Publicación