update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma
index 2154e4a559e5c6d5f6e0a728318ea530fa83ac75..0887edfc873412bede700a4d2a1b5e25b054bbf8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma
@@ -20,47 +20,47 @@ include "delayed_updating/substitution/lift_rmap.ma".
 rec definition lift_path (f) (p) on p: path ≝
 match p with
 [ list_empty     ⇒ (𝐞)
-| list_lcons l q ⇒ (lift_path f q)◖↑[↑[q]f]l
+| list_lcons l q ⇒ (lift_path f q)◖🠡[🠢[f]q]l
 ].
 
 interpretation
   "lift (path)"
-  'UpArrow f l = (lift_path f l).
+  'UpTriangleArrow f l = (lift_path f l).
 
 (* Basic constructions ******************************************************)
 
 lemma lift_path_empty (f):
-      (𝐞) = ↑[f]𝐞.
+      (𝐞) = 🠡[f]𝐞.
 // qed.
 
 lemma lift_path_rcons (f) (p) (l):
-      (↑[f]p)◖↑[↑[p]f]l = ↑[f](p◖l).
+      (🠡[f]p)◖🠡[🠢[f]p]l = 🠡[f](p◖l).
 // qed.
 
 lemma lift_path_d_dx (f) (p) (k):
-      (↑[f]p)◖𝗱((↑[p]f)＠⧣❨k❩) = ↑[f](p◖𝗱k).
+      (🠡[f]p)◖𝗱(🠢[f]p＠⧣❨k❩) = 🠡[f](p◖𝗱k).
 // qed.
 
 lemma lift_path_m_dx (f) (p):
-      (↑[f]p)◖𝗺 = ↑[f](p◖𝗺).
+      (🠡[f]p)◖𝗺 = 🠡[f](p◖𝗺).
 // qed.
 
 lemma lift_path_L_dx (f) (p):
-      (↑[f]p)◖𝗟 = ↑[f](p◖𝗟).
+      (🠡[f]p)◖𝗟 = 🠡[f](p◖𝗟).
 // qed.
 
 lemma lift_path_A_dx (f) (p):
-      (↑[f]p)◖𝗔 = ↑[f](p◖𝗔).
+      (🠡[f]p)◖𝗔 = 🠡[f](p◖𝗔).
 // qed.
 
 lemma lift_path_S_dx (f) (p):
-      (↑[f]p)◖𝗦 = ↑[f](p◖𝗦).
+      (🠡[f]p)◖𝗦 = 🠡[f](p◖𝗦).
 // qed.
 
 (* Constructions with path_append *******************************************)
 
 lemma lift_path_append (f) (p) (q):
-      (↑[f]p)●(↑[↑[p]f]q) = ↑[f](p●q).
+      (🠡[f]p)●(🠡[🠢[f]p]q) = 🠡[f](p●q).
 #f #p #q elim q -q //
 #l #q #IH
 <lift_path_rcons <lift_path_rcons
@@ -70,42 +70,42 @@ qed.
 (* Constructions with path_lcons ********************************************)
 
 lemma lift_path_lcons (f) (p) (l):
-      (↑[f]l)◗↑[↑[l]f]p = ↑[f](l◗p).
+      (🠡[f]l)◗🠡[🠢[f]l]p = 🠡[f](l◗p).
 #f #p #l
 <lift_path_append //
 qed.
 
 lemma lift_path_d_sn (f) (p) (k:pnat):
-      (𝗱(f＠⧣❨k❩)◗↑[⇂*[k]f]p) = ↑[f](𝗱k◗p).
+      (𝗱(f＠⧣❨k❩)◗🠡[⇂*[k]f]p) = 🠡[f](𝗱k◗p).
 // qed.
 
 lemma lift_path_m_sn (f) (p):
-      (𝗺◗↑[f]p) = ↑[f](𝗺◗p).
+      (𝗺◗🠡[f]p) = 🠡[f](𝗺◗p).
 // qed.
 
 lemma lift_path_L_sn (f) (p):
-      (𝗟◗↑[⫯f]p) = ↑[f](𝗟◗p).
+      (𝗟◗🠡[⫯f]p) = 🠡[f](𝗟◗p).
 // qed.
 
 lemma lift_path_A_sn (f) (p):
-      (𝗔◗↑[f]p) = ↑[f](𝗔◗p).
+      (𝗔◗🠡[f]p) = 🠡[f](𝗔◗p).
 // qed.
 
 lemma lift_path_S_sn (f) (p):
-      (𝗦◗↑[f]p) = ↑[f](𝗦◗p).
+      (𝗦◗🠡[f]p) = 🠡[f](𝗦◗p).
 // qed.
 
 (* Basic inversions *********************************************************)
 
 lemma lift_path_inv_empty (f) (p):
-      (𝐞) = ↑[f]p → 𝐞 = p.
+      (𝐞) = 🠡[f]p → 𝐞 = p.
 #f * // #p #l
 <lift_path_rcons #H0 destruct
 qed-.
 
 lemma lift_path_inv_rcons (f) (p2) (q1) (l1):
-      q1◖l1 = ↑[f]p2 →
-      ∃∃q2,l2. q1 = ↑[f]q2 & l1 = ↑[↑[q2]f]l2 & q2◖l2 = p2.
+      q1◖l1 = 🠡[f]p2 →
+      ∃∃q2,l2. q1 = 🠡[f]q2 & l1 = 🠡[🠢[f]q2]l2 & q2◖l2 = p2.
 #f * [| #l2 #q2 ] #q1 #l1
 [ <lift_path_empty
 | <lift_path_rcons
@@ -117,8 +117,8 @@ qed-.
 (* Inversions with path_append **********************************************)
 
 lemma lift_path_inv_append_sn (f) (q1) (r1) (p2):
-      q1●r1 = ↑[f]p2 →
-      ∃∃q2,r2. q1 = ↑[f]q2 & r1 = ↑[↑[q2]f]r2 & q2●r2 = p2.
+      q1●r1 = 🠡[f]p2 →
+      ∃∃q2,r2. q1 = 🠡[f]q2 & r1 = 🠡[🠢[f]q2]r2 & q2●r2 = p2.
 #f #q1 #r1 elim r1 -r1 [| #l1 #r1 #IH ] #p2
 [ <list_append_empty_sn #H0 destruct
   /2 width=5 by ex3_2_intro/
@@ -132,7 +132,7 @@ qed-.
 (* Main inversions **********************************************************)
 
 theorem lift_path_inj (f) (p1) (p2):
-        ↑[f]p1 = ↑[f]p2 → p1 = p2.
+        🠡[f]p1 = 🠡[f]p2 → p1 = p2.
 #f #p1 elim p1 -p1 [| #l1 #q1 #IH ] #p2
 [ <lift_path_empty #H0
   <(lift_path_inv_empty … H0) -H0 //