some renaming and some typos corrected ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lift_lift.ma

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 46b257efe94729c9e761fa2714fab0ba23615ed7..17aff3a81d8c4fe9d8e015bb8b30c06bb41a15d2 100644 (file)
--- 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.