include "ground/lib/stream_eq_eq.ma".
(* LIFT MAP FOR PATH ********************************************************)
(* Constructions with path_head *********************************************)
include "ground/lib/stream_eq_eq.ma".
(* LIFT MAP FOR PATH ********************************************************)
(* Constructions with path_head *********************************************)
@(stream_eq_trans … (tls_lift_rmap_d_dx …))
>nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
>nsucc_unfold /2 width=1 by/
@(stream_eq_trans … (tls_lift_rmap_d_dx …))
>nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
>nsucc_unfold /2 width=1 by/