- new component "s_transition" for the restored fqu and fquq

[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 ca66d927187fa9c13e52693e0510635578b8ef64..bb251965ed9f14bfcf95d668793d1ae1ce38c1ad 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,11 +20,11 @@ include "basic_2/reduction/cnx.ma".
 (* Advanced inversion lemmas on reducibility ********************************)
 
 (* Note: this property is unusual *)
-lemma cnx_inv_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⊥.
-#h #g #G #L #T #H elim H -L -T
-[ #L #k #d #Hkd #H
+lemma cnx_inv_crx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⊥.
+#h #o #G #L #T #H elim H -L -T
+[ #L #s #d #Hkd #H
   lapply (cnx_inv_sort … H) -H #H
-  lapply (deg_mono … H Hkd) -h -L -k <plus_n_Sm #H destruct
+  lapply (deg_mono … H Hkd) -h -L -s <plus_n_Sm #H destruct
 | #I #L #K #V #i #HLK #H
   elim (cnx_inv_delta … HLK H)
 | #L #V #T #_ #IHV #H