(⫯▶[f]p)@§❨m❩+♭q = ▶[f](p●𝗟◗q)@§❨m+n❩.
#o #f #p #q #m #n #Hn
/2 width=2 by nap_plus_unwind2_rmap_closed/
qed-.
lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
(⫯▶[f]p)@§❨m❩+♭q = ▶[f](p●𝗟◗q)@§❨m+n❩.
#o #f #p #q #m #n #Hn
/2 width=2 by nap_plus_unwind2_rmap_closed/
qed-.
lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):