我正在通过https://agda.readthedocs.io/en/v2.6.0.1/language/coinduction.html研究共形和协同模式。我以为我理解了本文的代码，所以我决定研究以下命题。
cons-uncons-id : ∀ {A} (xs : Stream A) → cons (uncons xs) ≈ xs
我以为这个主张与文章问题非常相似，也可以得到证明，但是我不能很好地证明这一主张。Here是我编写的代码。
我认为可以用cons-uncons-id (tl xs)进行细化，因为该类型与merge-split-id非常相似，但Agda不接受。
这是我想到的一个问题，所以我认为这是对的，但是当然存在误解的可能性。但是，优缺点和缺点会很自然地返回。
如果您应该能够在不被误解的情况下证明它，请告诉我如何证明它。
您能解释为什么不能以与merge-split-id相同的方式证明它吗？
关于，谢谢！
您只需要为refl自定义≈。
refl-≈ : ∀ {A} {xs : Stream A} → xs ≈ xs
hd-≈ refl-≈ = refl
tl-≈ refl-≈ = refl-≈
cons-uncons-id : ∀ {A} (xs : Stream A) → cons (uncons xs) ≈ xs
hd-≈ (cons-uncons-id _ ) = refl
tl-≈ (cons-uncons-id xs) = refl-≈
无法使用与merge-split-id相同的策略的原因是cons和uncons函数不会递归整个流（即，它们在第一个元素之后停止）。从某种意义上说，这实际上使cons-uncons-id引理更易于证明，因为您仅需证明第一个元素相等，然后其余的就是反射性。