我正在通过https://agda.readthedocs.io/en/v2.6.0.1/language/coinduction.html研究共导和共模式。我以为我理解文章代码，所以我决定研究以下命题。
cons-uncons-id : ? {A} (xs : Stream A) ? cons (uncons xs) ? xs
我以为这个命题和文章问题非常相似，也可以证明，但我不能很好地证明。 这是我写的代码。
我认为它可以改进，cons-uncons-id (tl xs)因为它的类型与 merge-split-id 非常相似，但 Agda 不接受它。
这是我自己想到的一个问题，所以我认为这是真的，但当然存在误解的可能性。然而，非利弊和利弊会恢复原状是很自然的。
如果你应该能够证明它而不会被误解，请告诉我你如何证明它。
你能解释一下为什么不能像merge-split-id一样证明吗？
问候，谢谢！