+
+lemma unwind2_rmap_append_closed_Lq_dx_nap_plus (f) (p) (q) (m) (n):
+ q ϵ 𝐂❨n❩ →
+ ▶[f]p@❨m❩+♭q = ▶[f](p●𝗟◗q)@§❨m+n❩.
+#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=1 by unwind2_rmap_append_closed_Lq_dx_nap_depth/
+]
+qed-.