(**************************************************************************)
include "delayed_updating/substitution/lift.ma".
+include "ground/relocation/tr_uni_compose.ma".
+include "ground/relocation/tr_compose_compose.ma".
include "ground/relocation/tr_compose_eq.ma".
include "ground/relocation/tr_pn_eq.ma".
lemma lift_path_S_sn (f) (p):
(š¦āā[f]p) = ā[f](š¦āp).
// qed.
+
+lemma lift_path_after (p) (f1) (f2):
+ ā[f2]ā[f1]p = ā[f2āf1]p.
+#p @(path_ind_lift ā¦ p) -p // [ #n #l #p | #p ] #IH #f1 #f2
+[ <lift_path_d_lcons_sn <lift_path_d_lcons_sn
+ >(lift_path_eq_repl ā¦ (tr_compose_assoc ā¦)) //
+| <lift_path_L_sn <lift_path_L_sn <lift_path_L_sn
+ >tr_compose_push_bi //
+]
+qed.
+
+(* Advanced constructions with proj_rmap and stream_tls *********************)
+
+lemma lift_rmap_tls_d_dx (f) (p) (m) (n):
+ ā*[m+n]ā[p]f ā ā*[m]ā[pāš±n]f.
+#f #p #m #n
+<lift_rmap_d_dx >nrplus_inj_dx
+/2 width=1 by tr_tls_compose_uni_dx/
+qed.