update in binararies for λδ

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / computation / cprs_lift.ma

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 635f1e237f63a97ff26c90023f7d50897be3086b..21e162440c8367e90d90239cf932bc75161bec7f 100644 (file)
--- 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.