CoinductiveConstructorsAndLet.err

CoinductiveConstructorsAndLet.agda:8,22-25
Not implemented: coinductive constructor in the scope of a
let-bound variable
when checking that the expression ♯ y has type ∞ D