-lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (k):
- p = (↳[n]p)●q → k ≤ n →
- (▶[f]p)@❨k❩ = (▶[f]↳[n]p)@❨k❩.
-#f #p elim p -p
-[ #q #n #k #Hq #Hk
- elim (eq_inv_list_empty_append … Hq) -Hq * #_ //
-| #l #p #IH #q #n @(nat_ind_succ … n) -n
- [ #k #_ #Hk <(nle_inv_zero_dx … Hk) -k -IH
- <path_head_zero <unwind2_rmap_empty //
- | #n #_ #k cases l [ #m ]
- [ <path_head_d_sn <list_append_lcons_sn #Hq #Hk
+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