Hello,

does anyone have an idea on how the following proof can be completed:

****

CoInductive stream ( T : UU ) := streamconstr : forall ( t : T ) ( s : stream T ) , stream T .

Definition streamfunct { T1 T2 : UU } ( f : T1 -> T2 ) ( s1 : stream T1 ) : stream T2 .
Proof. intros . cofix. destruct s1 as [ s1f s1r ] . exact ( streamconstr T2 ( f s1f ) streamfunct ) . Defined .

Lemma streamfunctid { T : UU } ( s : stream T ) : paths ( streamfunct ( idfun T ) s ) s .
Proof.  intros .  ???

****

V.

PS  "idfun T := fun x : T => x" and "paths" is a notation for identity.