Finalized copy sub-machine of the universal turing machine. Some new results

[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 33c6455dc53261f84b5ccbd818e21882af849bf4..3cd83733e7a395528779bf151835fa464ca10dd4 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
@@ -121,7 +121,7 @@ lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
 lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1.
                             L ⊢ ⬇* 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 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
 @csn_intro #X #HL #H
 elim (cpr_inv_appl1_simple … HL ?) -HL //