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
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