X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcsn_lift.ma;h=85cdef226346824371ae67c4723e16c85a1d9b54;hb=5ac2dc4e01aca542ddd13c02b304c646d8df9799;hp=71b4d33802ede2b61161d4e8ccea3eeb0cefff61;hpb=a386e0eb6b20909ae78c825203d77647b8fde30c;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
index 71b4d3380..85cdef226 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
@@ -71,7 +71,7 @@ qed.
 
 lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1.
                        (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) →
-                       𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
+                       𝐒⦃T1⦄ → L ⊢ ⬇* ⓐV. T1.
 #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1
 @csn_intro #X #H1 #H2
 elim (cpr_inv_appl1_simple … H1 ?) // -H1