X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fcomputation%2Fcprs_lift.ma;h=21e162440c8367e90d90239cf932bc75161bec7f;hp=635f1e237f63a97ff26c90023f7d50897be3086b;hb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea;hpb=3a4509b8e569181979f5b15808361c83eb1ae49a

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/cprs_lift.ma
index 635f1e237..21e162440 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/cprs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/cprs_lift.ma
@@ -19,7 +19,6 @@ include "basic_2A/computation/cprs.ma".
 
 (* Advanced properties ******************************************************)
 
-(* Note: apparently this was missing in basic_1 *)
 lemma cprs_delta: ∀G,L,K,V,V2,i.
                   ⬇[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡* V2 →
                   ∀W2. ⬆[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡* W2.