帰導型に関する「帰導原理」を証明できますか? たとえば、ストリーム タイプの結合原理の擬似コードは次のようになります。
Π P : Stream A -> Type.
Π destruct_head : Π x : Stream A. P x -> Σ y : A. Path A (head x) y.
Π destruct_tail : Π x : Stream A. P x -> P (tail x).
(Σ y : Stream A. P y)
これは正しいと思いますが、Coq や Agda でそれを証明する方法が思いつきません。