- Properties S3 and S5 of context-sensitive strongly normalizing terms

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / csn_lcpr.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma
index 28b9245ca049651ff0afbed9e5c5af9e8c57a6e9..c6024fce8d26579227d6b7484aa149b000d9c2b2 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma
@@ -113,7 +113,6 @@ elim (cpr_inv_appl1 … HL) -HL *
 ]
 qed.
 
-(* Basic_1: was: sn3_appl_bind *)
 lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
                       ∀L,V,T. L ⊢ ⬇* ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T.
 /2 width=5/ qed.