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 13e746d7fc05bd8104ae62444dab0e551bb52a9d..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
@@ -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⦄ →