1 include "delayed_updating/substitution/lift_eq.ma".
2 include "delayed_updating/syntax/path_head.ma".
3 include "delayed_updating/syntax/path_reverse.ma".
4 include "ground/relocation/xap.ma".
6 axiom tr_xap_succ_pos (f) (n):
9 axiom tr_xap_plus (n1) (n2) (f):
10 (⇂*[n2]f)@❨n1❩+f@❨n2❩ = f@❨n1+n2❩.
12 axiom eq_inv_path_empty_head (p) (n):
15 lemma lift_path_head (f) (p) (q) (n):
17 ↳[↑[q●p]f@❨n❩](↑[f](q●p))ᴿ = (↑[↑[q]f]p)ᴿ.
18 #f #p @(list_ind_rcons … p) -p
20 <(eq_inv_path_empty_head … H0) -H0
22 | #p #l #IH #q #n @(nat_ind_succ …n) -n [| #m #_ ]
23 [ <reverse_rcons <path_head_zero #H0 destruct
25 [ <reverse_rcons <path_head_d_sn #H0
26 elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
27 <list_append_assoc <lift_rmap_d_dx <lift_path_d_dx <reverse_rcons
28 <tr_xap_succ_pos <path_head_d_sn >tr_xap_succ_pos
29 <lift_path_d_dx >lift_rmap_append <reverse_rcons
30 @eq_f2 // <(IH … H0) -IH -H0
31 @eq_f2 // <tr_xap_plus //