X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcsn_lcpr.ma;h=3cd83733e7a395528779bf151835fa464ca10dd4;hb=69644bb333b2862a5ff2ff434df8830e854e3385;hp=169073516d2f5730b6a2ba0406244049d555fec2;hpb=2ba7ef901a6b72210692792f2396c08bc0cff52c;p=helm.git

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 169073516..3cd83733e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma
@@ -120,8 +120,8 @@ lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
 (* Basic_1: was only: sn3_appl_appl *)
 lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1.
                             L ⊢ ⬇* T1 →
-                            (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) →
-                            𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
+                            (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) →
+                            𝐒⦃T1⦄ → L ⊢ ⬇* ⓐV. T1.
 #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
 @csn_intro #X #HL #H
 elim (cpr_inv_appl1_simple … HL ?) -HL //