+
+lemma unwind2_rmap_append_closed_bLq_dx_nap_plus (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
+>(unwind2_rmap_append_closed_true_dx_xap_depth f p … Hb) -Hb
+>(unwind2_rmap_append_closed_Lq_dx_nap_plus … 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
+@(stream_eq_trans … (tls_unwind2_rmap_append_closed_true_dx … Hb)) -Hb
+@stream_tls_eq_repl
+@(stream_eq_trans … (tls_succ_unwind2_rmap_append_closed_Lq_dx … Hq)) -Hq //
+qed-.