+/2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
+qed-.
+
+lemma tls_unwind2_rmap_append_closed_true_dx (f) (p) (q) (n):
+ q ϵ 𝐂❨Ⓣ,n❩ →
+ ▶[f]p ≗ ⇂*[n]▶[f](p●q).
+/2 width=1 by tls_plus_unwind2_rmap_closed_true/
+qed-.
+
+lemma nap_plus_unwind2_rmap_append_closed_Lq_dx_depth (o) (f) (p) (q) (m) (n):
+ q ϵ 𝐂❨o,n❩ →
+ ▶[f]p@❨m❩+♭q = ▶[f](p●𝗟◗q)@§❨m+n❩.
+#o #f #p #q #m #n #Hq
+<tr_nap_plus @eq_f2
+[ <(tr_xap_eq_repl … (tls_succ_unwind2_rmap_append_closed_Lq_dx …)) //
+| /2 width=2 by nap_unwind2_rmap_append_closed_Lq_dx_depth/
+]
+qed-.
+
+lemma nap_plus_unwind2_rmap_append_closed_bLq_dx_depth (o) (f) (p) (b) (q) (m) (n):
+ b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
+ ♭b+♭q = ▶[f](p●b●𝗟◗q)@§❨m+n❩.
+#o #f #p #b #q #m #n #Hb #Hq
+>(xap_unwind2_rmap_append_closed_true_dx_depth f p … Hb) -Hb
+>(nap_plus_unwind2_rmap_append_closed_Lq_dx_depth … Hq) -Hq //
+qed-.
+
+lemma tls_succ_plus_unwind2_rmap_append_closed_bLq_dx (o) (f) (p) (b) (q) (m) (n):
+ b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
+ ▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●b●𝗟◗q).
+#o #f #p #b #q #m #n #Hb #Hq
+>nplus_succ_dx <stream_tls_plus >list_append_assoc
+@(stream_eq_trans … (tls_unwind2_rmap_append_closed_true_dx … Hb)) -Hb
+/3 width=2 by stream_tls_eq_repl, tls_succ_unwind2_rmap_append_closed_Lq_dx/