- the shift function is now defined and cpr_shift_fwd is proved

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / grammar / lenv_length.ma

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma
index 437730a83301baef415e65a4d77c1bc982d051e5..2321e7b0d760da23e4cb2adf0ce86ab4983da3ea 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma
@@ -14,9 +14,8 @@
 
 include "Basic-2/grammar/lenv.ma".
 
-(* LENGTH *******************************************************************)
+(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
 
-(* the length of a local environment *)
 let rec length L ≝ match L with
 [ LSort       ⇒ 0
 | LPair L _ _ ⇒ length L + 1