X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_structure.ma;h=86a4259758106db83442adc285d8af1a472cc3f2;hb=d59f1c74c62ad3706d50707bb68758d88fbed006;hp=961a5c435ef8b0f3d2cbd106a5bc80279ccf85db;hpb=ac8d0dc0c6fb995736e0c10486d996bd023f3c32;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
index 961a5c435..86a425975 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
@@ -14,55 +14,22 @@
 
 include "delayed_updating/substitution/lift_eq.ma".
 include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/syntax/path_proper.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
-(* Basic constructions with structure **************************************)
+(* Constructions with structure ********************************************)
 
 lemma structure_lift (p) (f):
       ⊗p = ⊗↑[f]p.
-#p @(path_ind_lift … p) -p // #p #IH #f
-<lift_path_L_sn //
+#p elim p -p //
+* [ #n ] #p #IH #f //
+[ <lift_path_m_sn <structure_m_sn <structure_m_sn //
+| <lift_path_L_sn <structure_L_sn <structure_L_sn //
+]
 qed.
 
 lemma lift_structure (p) (f):
       ⊗p = ↑[f]⊗p.
-#p @(path_ind_lift … p) -p //
-qed.
-
-(* Properties with proper condition for path ********************************)
-
-lemma lift_append_proper_dx (p2) (p1) (f): Ꝕp2 →
-      (⊗p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
-#p2 #p1 @(path_ind_lift … p1) -p1 //
-[ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
-[ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
-| <lift_path_d_lcons_sn <IH //
-| <lift_path_L_sn <IH //
-| <lift_path_A_sn <IH //
-| <lift_path_S_sn <IH //
-]
-qed-.
-
-(* Advanced constructions with structure ************************************)
-
-lemma lift_d_empty_dx (n) (p) (f):
-      (⊗p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
-qed.
-
-lemma lift_L_dx (p) (f):
-      (⊗p)◖𝗟 = ↑[f](p◖𝗟).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
-qed.
-
-lemma lift_A_dx (p) (f):
-      (⊗p)◖𝗔 = ↑[f](p◖𝗔).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
-qed.
-
-lemma lift_S_dx (p) (f):
-      (⊗p)◖𝗦 = ↑[f](p◖𝗦).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
+#p elim p -p //
+* [ #n ] #p #IH #f //
 qed.