- relation between native type and atomic arity proced

[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 169073516d2f5730b6a2ba0406244049d555fec2..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
@@ -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 //