include "delayed_updating/unwind2/unwind_depth.ma".
include "ground/relocation/tr_uni_compose.ma".

lemma pippo (q) (p): 
      ▼[p]𝐢 ≗ ⇂*[↑❘q❘]▼[p●𝗟◗q]𝐢.
#q @(list_ind_rcons … q) -q //
#q * [ #n ] #IH #p //
<depth_d_dx >list_cons_shift <list_append_assoc
<unwind_rmap_d_dx
check tr_tls_compose_uni_sn