update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
index 9c4b0f3b5ac350eba4175d9fc10d603361a96d4f..f6759bd1e0fd1f7011adc2bd9116177771628903 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -15,7 +15,6 @@
 include "delayed_updating/substitution/lift.ma".
 include "ground/relocation/tr_pap_eq.ma".
 include "ground/relocation/tr_pn_eq.ma".
-include "ground/lib/stream_tls_eq.ma".
 
 (* LIFT FOR PATH ************************************************************)
 
@@ -34,7 +33,7 @@ lemma lift_eq_repl (A) (p) (k1) (k2):
 #k1 #k2 #Hk #f1 #f2 #Hf
 [ <lift_empty <lift_empty /2 width=1 by/
 | <lift_d_sn <lift_d_sn <(tr_pap_eq_repl … Hf)
-  /3 width=3 by stream_tls_eq_repl, compose_repl_fwd_sn/
+  /3 width=1 by stream_eq_refl/
 | /3 width=1 by/
 | /3 width=1 by tr_push_eq_repl/
 | /3 width=1 by/
@@ -87,7 +86,7 @@ lemma lift_path_lcons (f) (p) (l):
 qed.
 
 lemma lift_path_d_sn (f) (p) (n):
-      (𝗱(f＠⧣❨n❩)◗↑[⇂*[n]f]p) = ↑[f](𝗱n◗p).
+      (𝗱(f＠⧣❨n❩)◗↑[𝐢]p) = ↑[f](𝗱n◗p).
 // qed.
 
 lemma lift_path_m_sn (f) (p):
@@ -106,6 +105,15 @@ lemma lift_path_S_sn (f) (p):
       (𝗦◗↑[f]p) = ↑[f](𝗦◗p).
 // qed.
 
+lemma lift_path_id (p):
+      p = ↑[𝐢]p.
+#p elim p -p //
+* [ #n ] #p #IH //
+[ <lift_path_d_sn //
+| <lift_path_L_sn //
+]
+qed.
+
 lemma lift_path_append (p2) (p1) (f):
       (↑[f]p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
 #p2 #p1 elim p1 -p1 //
@@ -118,29 +126,29 @@ lemma lift_path_append (p2) (p1) (f):
 ]
 qed.
 
-lemma lift_path_d_dx (f) (p) (n):
+lemma lift_path_d_dx (n) (p) (f):
       (↑[f]p)◖𝗱((↑[p]f)＠⧣❨n❩) = ↑[f](p◖𝗱n).
-#f #p #n <lift_path_append //
+#n #p #f <lift_path_append //
 qed.
 
-lemma lift_path_m_dx (f) (p):
+lemma lift_path_m_dx (p) (f):
       (↑[f]p)◖𝗺 = ↑[f](p◖𝗺).
-#f #p <lift_path_append //
+#p #f <lift_path_append //
 qed.
 
-lemma lift_path_L_dx (f) (p):
+lemma lift_path_L_dx (p) (f):
       (↑[f]p)◖𝗟 = ↑[f](p◖𝗟).
-#f #p <lift_path_append //
+#p #f <lift_path_append //
 qed.
 
-lemma lift_path_A_dx (f) (p):
+lemma lift_path_A_dx (p) (f):
       (↑[f]p)◖𝗔 = ↑[f](p◖𝗔).
-#f #p <lift_path_append //
+#p #f <lift_path_append //
 qed.
 
-lemma lift_path_S_dx (f) (p):
+lemma lift_path_S_dx (p) (f):
       (↑[f]p)◖𝗦 = ↑[f](p◖𝗦).
-#f #p <lift_path_append //
+#p #f <lift_path_append //
 qed.
 
 (* COMMENT 
@@ -153,5 +161,4 @@ lemma lift_rmap_tls_d_dx (f) (p) (m) (n):
 <lift_rmap_d_dx >nrplus_inj_dx
 /2 width=1 by tr_tls_compose_uni_dx/
 qed.
-
 *)