X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Flift_lift.ma;h=17aff3a81d8c4fe9d8e015bb8b30c06bb41a15d2;hb=7e06d9d148ae04a21943377debd933a742d0c2fa;hp=46b257efe94729c9e761fa2714fab0ba23615ed7;hpb=3167db4903eea2eddc60a91cfd922be3672ce077;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
index 46b257efe..17aff3a81 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
@@ -16,7 +16,7 @@ include "basic_2/substitution/lift.ma".
 
 (* BASIC TERM RELOCATION ****************************************************)
 
-(* Main properies ***********************************************************)
+(* Main properties ***********************************************************)
 
 (* Basic_1: was: lift_inj *)
 theorem lift_inj: ∀d,e,T1,U. ⇧[d,e] T1 ≡ U → ∀T2. ⇧[d,e] T2 ≡ U → T1 = T2.