update in basic_2 and ground_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cnx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma
index 5aa9c97100ad949f2e7c6c8dbd3f4f5705c190c6..cc2397d0f8dbf569165da561cac9bd99fc340cb1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/predtynormal_5.ma".
-include "basic_2/syntax/tdeq.ma".
+include "static_2/syntax/tdeq.ma".
 include "basic_2/rt_transition/cpx.ma".
 
 (* NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ********)
@@ -33,7 +33,7 @@ lapply (H (⋆(next h s)) ?) -H /2 width=2 by cpx_ess/ -G -L #H
 elim (tdeq_inv_sort1 … H) -H #s0 #d #H1 #H2 #H destruct
 lapply (deg_next … H1) #H0
 lapply (deg_mono … H0 … H2) -H0 -H2 #H
-<(pred_inv_refl … H) -H //
+>(pred_inv_fix_sn … H) -H //
 qed-.
 
 lemma cnx_inv_abst: ∀h,o,p,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓛ{p}V.T⦄ →