2 f@āØšā©āØ®āf = f.
6 corec lemma tr_compose_id_dx (f):
9 cases tr_compose_unfold
10 cases (pippo f) in ā¢ (??%?);
11 @stream_eq_cons /2 width=1 by/
15 f@āØpā© + (ā*[ninj p]f)@āØšā© = f@āØāpā©.
18 (š¢) = āš®āØnā©.
21 axiom tr_uni_tls_pos (p:pnat) (n):
22 (š¢) = ā*[p]š®āØnā©.
25 >nsucc_pnpred <stream_tls_swap