update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / lift.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index 3a6991a92d686797e9862700bbaea455e8e5230f..bfb66f1bc911e23f4b6a2b445f62fe236f6552c4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -144,6 +144,28 @@ lemma lift_rmap_append (p2) (p1) (f):
 ]
 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.
+
 (* Advanced eliminations with path ******************************************)
 
 lemma path_ind_lift (Q:predicate …):