InductiveAndCoinductiveConstructors.err

InductiveAndCoinductiveConstructors.agda:62,25-66
.InductiveAndCoinductiveConstructors.♯-4 xs ls !=
.InductiveAndCoinductiveConstructors.♯-3 xs ls of type
∞ (WHNF (stream (stream unit)))
when checking that the expression
lemma xs (↓ ♯ (ls ≺ snd (label xs ls))) has type
⟦ fst (label xs ls) ⟧ ≈ ⟦ xs ⟧