+
+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/
+qed-.