X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_path.ma;h=0887edfc873412bede700a4d2a1b5e25b054bbf8;hp=2154e4a559e5c6d5f6e0a728318ea530fa83ac75;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hpb=d06053844638d88936d711b66fddbcca2a9add1c

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 2154e4a55..0887edfc8 100644
--- 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 //