+lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (m):
+ q = ↳[n]q → m ≤ n →
+ ▶[f](p●q)@❨m❩ = ▶[f]↳[n](p●q)@❨m❩.
+#f #p #q elim q -q
+[ #n #m #Hq
+ <(eq_inv_path_empty_head … Hq) -n #Hm
+ <(nle_inv_zero_dx … Hm) -m //
+| #l #q #IH #n @(nat_ind_succ … n) -n
+ [ #m #_ #Hm <(nle_inv_zero_dx … Hm) -m -IH //
+ | #n #_ #m cases l [ #k ]
+ [ <path_head_d_dx #Hq #Hm
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ <unwind2_rmap_d_dx <unwind2_rmap_d_dx
+ <tr_compose_xap <tr_compose_xap
+ @(IH … Hq) -IH -Hq (**) (* auto too slow *)
+ @nle_trans [| @tr_uni_xap ]
+ /2 width=1 by nle_plus_bi_dx/
+ | <path_head_m_dx #Hq #Hm
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ <unwind2_rmap_m_dx <unwind2_rmap_m_dx
+ /2 width=2 by/
+ | <path_head_L_dx #Hq
+ @(nat_ind_succ … m) -m // #m #_ #Hm
+ lapply (nle_inv_succ_bi … Hm) -Hm #Hm
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ <unwind2_rmap_L_dx <unwind2_rmap_L_dx
+ <tr_xap_push <tr_xap_push
+ /3 width=2 by eq_f/
+ | <path_head_A_dx #Hq #Hm
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ <unwind2_rmap_A_dx <unwind2_rmap_A_dx
+ /2 width=2 by/
+ | <path_head_S_dx #Hq #Hm
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ <unwind2_rmap_S_dx <unwind2_rmap_S_dx
+ /2 width=2 by/
+ ]
+ ]
+]
+qed-.
+
+lemma unwind2_rmap_head_xap_closed (f) (p) (q) (n):
+ q = ↳[n]q →
+ ▶[f](p●q)@❨n❩ = ▶[f]↳[n](p●q)@❨n❩.
+/2 width=2 by unwind2_rmap_head_xap_le_closed/
+qed-.
+
+lemma unwind2_rmap_head_xap (f) (p) (n):
+ n + ♯(↳[n]p) = (▶[f]↳[n]p)@❨n❩.