* #p #f //
qed.
-corec lemma tr_compose_id_dx (f):
- f ā fāš¢.
-cases tr_id_unfold
-cases tr_compose_unfold
-cases (pippo f) in ā¢ (??%?);
-@stream_eq_cons /2 width=1 by/
-qed.
-
axiom pippo2 (f) (p):
f@āØpā© + (ā*[ninj p]f)@āØšā© = f@āØāpā©.