partial commit: just the components before "static" ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
index 99ca32c13ad78a464ae0ab1e1e6ed70e176872f4..84951db3482b538fd0c699c2e1c6a57c8d6c612d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
@@ -20,7 +20,7 @@ include "basic_2/reduction/cnx.ma".
 (* Advanced inversion lemmas on context-sensitive reducible terms ***********)
 
 (* Note: this property is unusual *)
-lemma cnx_inv_crx: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⊥.
+lemma cnx_inv_crx: ∀h,g,L,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⊥.
 #h #g #L #T #H elim H -L -T
 [ #L #k #l #Hkl #H
   lapply (cnx_inv_sort … H) -H #H