commit of the "computation" component with lazy pointwise extensions

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / csx_alt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma
index df23e1f2ab9374774ace93fe4073ae840611560a..a6f46c787c3f8b782053636d3d956e197c8d9627 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma
@@ -38,7 +38,7 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma csx_intro_cprs: ∀h,g,G,L,T1.
+lemma csx_intro_cpxs: ∀h,g,G,L,T1.
                          (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] T2) →
                       ⦃G, L⦄ ⊢ ⬊*[h, g] T1.
 /4 width=1 by cpx_cpxs, csx_intro/ qed.