update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma
index be57d860180a561ba424518e904d247acca207d1..8dc8af8f8448c1bd4ca693fc2ee4304eb34075fd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/notation/functions/uparrow_2.ma".
+include "delayed_updating/notation/functions/uptrianglearrow_2.ma".
 include "delayed_updating/syntax/label.ma".
 include "ground/relocation/tr_pap_pap.ma".
 
@@ -29,34 +29,34 @@ match l with
 
 interpretation
   "prelift (label)"
-  'UpArrow f l = (prelift_label f l).
+  'UpTriangleArrow f l = (prelift_label f l).
 
 (* Basic constructions ******************************************************)
 
 lemma prelift_label_d (f) (k):
-      (𝗱(f＠⧣❨k❩)) = ↑[f]𝗱k.
+      (𝗱(f＠⧣❨k❩)) = 🠡[f]𝗱k.
 // qed.
 
 lemma prelift_label_m (f):
-      (𝗺) = ↑[f]𝗺.
+      (𝗺) = 🠡[f]𝗺.
 // qed.
 
 lemma prelift_label_L (f):
-      (𝗟) = ↑[f]𝗟.
+      (𝗟) = 🠡[f]𝗟.
 // qed.
 
 lemma prelift_label_A (f):
-      (𝗔) = ↑[f]𝗔.
+      (𝗔) = 🠡[f]𝗔.
 // qed.
 
 lemma prelift_label_S (f):
-      (𝗦) = ↑[f]𝗦.
+      (𝗦) = 🠡[f]𝗦.
 // qed.
 
 (* Basic inversions *********************************************************)
 
 lemma prelift_label_inv_d_sn (f) (l) (k1):
-      (𝗱k1) = ↑[f]l →
+      (𝗱k1) = 🠡[f]l →
       ∃∃k2. k1 = f＠⧣❨k2❩ & 𝗱k2 = l.
 #f * [ #k ] #k1
 [ <prelift_label_d
@@ -69,7 +69,7 @@ lemma prelift_label_inv_d_sn (f) (l) (k1):
 qed-.
 
 lemma prelift_label_inv_m_sn (f) (l):
-      (𝗺) = ↑[f]l → 𝗺 = l.
+      (𝗺) = 🠡[f]l → 𝗺 = l.
 #f * [ #k ]
 [ <prelift_label_d
 | <prelift_label_m
@@ -80,7 +80,7 @@ lemma prelift_label_inv_m_sn (f) (l):
 qed-.
 
 lemma prelift_label_inv_L_sn (f) (l):
-      (𝗟) = ↑[f]l → 𝗟 = l.
+      (𝗟) = 🠡[f]l → 𝗟 = l.
 #f * [ #k ]
 [ <prelift_label_d
 | <prelift_label_m
@@ -91,7 +91,7 @@ lemma prelift_label_inv_L_sn (f) (l):
 qed-.
 
 lemma prelift_label_inv_A_sn (f) (l):
-      (𝗔) = ↑[f]l → 𝗔 = l.
+      (𝗔) = 🠡[f]l → 𝗔 = l.
 #f * [ #k ]
 [ <prelift_label_d
 | <prelift_label_m
@@ -102,7 +102,7 @@ lemma prelift_label_inv_A_sn (f) (l):
 qed-.
 
 lemma prelift_label_inv_S_sn (f) (l):
-      (𝗦) = ↑[f]l → 𝗦 = l.
+      (𝗦) = 🠡[f]l → 𝗦 = l.
 #f * [ #k ]
 [ <prelift_label_d
 | <prelift_label_m
@@ -115,7 +115,7 @@ qed-.
 (* Main inversions **********************************************************)
 
 theorem prelift_label_inj (f) (l1) (l2):
-        ↑[f]l1 = ↑[f]l2 → l1 = l2.
+        🠡[f]l1 = 🠡[f]l2 → l1 = l2.
 #f * [ #k1 ] #l2 #Hl
 [ elim (prelift_label_inv_d_sn … Hl) -Hl #k2 #Hk #H0 destruct
   >(tr_pap_inj ???? Hk) -Hk //