[ @(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
>nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold //
| <unwind2_rmap_L_dx <nplus_succ_dx //
]
qed-.
[ @(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
>nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold //
| <unwind2_rmap_L_dx <nplus_succ_dx //
]
qed-.