X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fsubstitution%2Flift_fun.ma;h=58d718fb7f6bfc9562e18bec49992ce252fe4321;hb=f9201115d73cc65ab2aadc1a7c94cd52564d3b2e;hp=0044de7f1c1d4ef744782ba586c4e23b705787bc;hpb=6e150e6a7760f2670d3537a20e16d251e71d7506;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/substitution/lift_fun.ma b/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
index 0044de7f1..58d718fb7 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
@@ -16,7 +16,7 @@ include "lambda-delta/substitution/lift_defs.ma".
 
 (* RELOCATION ***************************************************************)
 
-(* the functional properties ************************************************)
+(* Functional properties ****************************************************)
 
 lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2.
 #T1 elim T1 -T1