bug fix in the notation of normal forms, now we specify that they are

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cnx_cix.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma
index 3e62a5c60bc43a5abde3b69b67382b46207ec301..18dc60e3e8d23c7a3514d0b28b90f30804a680e1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma
@@ -19,10 +19,10 @@ include "basic_2/reduction/cnx_crx.ma".
 
 (* Main properties on context-sensitive extended irreducible terms **********)
 
-theorem cix_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄.
+theorem cix_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄.
 /2 width=6 by cpx_fwd_cix/ qed.
 
 (* Main inversion lemmas on context-sensitive extended irreducible terms ****)
 
-theorem cnr_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄.
+theorem cnr_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
 /2 width=7 by cnx_inv_crx/ qed-.