X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts.ma;h=9116951c311d6da1f41ca06af4caad072b44c51b;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=1b383569934c5ff49afe90c9b24b45705b723590;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
index 1b3835699..9116951c3 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
@@ -41,7 +41,7 @@ interpretation "generic relocation (term)"
    'RLiftStar f T1 T2 = (lifts f T1 T2).
 
 definition liftable2_sn: predicate (relation term) ≝
-                         λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 → 
+                         λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 →
                          ∃∃U2. ⇧*[f] T2 ≘ U2 & R U1 U2.
 
 definition deliftable2_sn: predicate (relation term) ≝
@@ -49,7 +49,7 @@ definition deliftable2_sn: predicate (relation term) ≝
                            ∃∃T2. ⇧*[f] T2 ≘ U2 & R T1 T2.
 
 definition liftable2_bi: predicate (relation term) ≝
-                         λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 → 
+                         λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 →
                          ∀U2. ⇧*[f] T2 ≘ U2 → R U1 U2.
 
 definition deliftable2_bi: predicate (relation term) ≝
@@ -486,8 +486,8 @@ lemma lifts_uni: ∀n1,n2,T,U. ⇧*[𝐔❴n1❵∘𝐔❴n2❵] T ≘ U → ⇧
               lift_lref_ge_minus lift_lref_ge_minus_eq
 *)
 (* Basic_1: removed theorems 8:
-            lift_lref_gt            
-            lift_head lift_gen_head 
+            lift_lref_gt
+            lift_head lift_gen_head
             lift_weight_map lift_weight lift_weight_add lift_weight_add_O
             lift_tlt_dx
 *)