some resuls on pointwise extensions (all of them are now in the

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
index ec36d47f1432e71b0685fbf8d2607ed5e4b7cf60..76b8cc8ad3a15d938a201c8b3c81f9d64be7e38d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
@@ -13,13 +13,13 @@
 (**************************************************************************)
 
 include "basic_2/grammar/tstc.ma".
-include "basic_2/computation/lpxs_cpxs.ma".
+include "basic_2/computation/llpxs_cpxs.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
 
 (* Forward lemmas involving same top term constructor ***********************)
 
-lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≃ U.
+lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≃ U.
 #h #g #G #L #T #HT #U #H
 >(cpxs_inv_cnx1 … H HT) -G -L -T //
 qed-.