#p elim p -p [| #p #IH ] * #q1 #f1 #f2 //
<tr_compose_unfold <tr_pap_succ
>nsucc_inj <stream_tls_succ_lcons <stream_tls_succ_lcons
#p elim p -p [| #p #IH ] * #q1 #f1 #f2 //
<tr_compose_unfold <tr_pap_succ
>nsucc_inj <stream_tls_succ_lcons <stream_tls_succ_lcons