(* *)
(**************************************************************************)
-include "ground/relocation/tr_compose.ma".
-include "ground/relocation/tr_uni.ma".
+include "ground/relocation/tr_compose_pap.ma".
+include "ground/relocation/tr_uni_pap.ma".
include "delayed_updating/syntax/path.ma".
include "delayed_updating/notation/functions/uparrow_4.ma".
include "delayed_updating/notation/functions/uparrow_2.ma".
(* Basic constructions with proj_rmap ***************************************)
+lemma lift_rmap_empty (f):
+ f = โ[๐]f.
+// qed.
+
lemma lift_rmap_d_sn (f) (p) (n):
โ[p](fโ๐ฎโจninj nโฉ) = โ[๐ฑnโp]f.
#f * // qed.
]
qed.
+(* Advanced constructions with proj_rmap and path_rcons *********************)
+
+lemma lift_rmap_d_dx (f) (p) (n):
+ (โ[p]f)โ๐ฎโจninj nโฉ = โ[pโ๐ฑn]f.
+// qed.
+
+lemma lift_rmap_m_dx (f) (p):
+ โ[p]f = โ[pโ๐บ]f.
+// qed.
+
+lemma lift_rmap_L_dx (f) (p):
+ (โซฏโ[p]f) = โ[pโ๐]f.
+// qed.
+
+lemma lift_rmap_A_dx (f) (p):
+ โ[p]f = โ[pโ๐]f.
+// qed.
+
+lemma lift_rmap_S_dx (f) (p):
+ โ[p]f = โ[pโ๐ฆ]f.
+// qed.
+
+lemma lift_rmap_pap_d_dx (f) (p) (n) (m):
+ โ[p]f@โจm+nโฉ = โ[pโ๐ฑn]f@โจmโฉ.
+#f #p #n #m
+<lift_rmap_d_dx <tr_compose_pap <tr_uni_pap //
+qed.
+
(* Advanced eliminations with path ******************************************)
lemma path_ind_lift (Q:predicate โฆ):