- nDestructTac: Sys.break handled in two places

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

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 71b4d33802ede2b61161d4e8ccea3eeb0cefff61..85cdef226346824371ae67c4723e16c85a1d9b54 100644 (file)
--- 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