- name changes in the rediction rules

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cpxs_tstc.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
index eed76daea80e3c4738a0b34c453372d645c65f82..c0a202ae5db8fd6b56f6b89d86e555bcc8a08566 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
@@ -34,7 +34,7 @@ elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus 
   elim (IHn … Hnl) -IHn
   [ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/
   | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n
-    /4 width=3 by cpxs_strap2, cpx_sort, or_intror/
+    /4 width=3 by cpxs_strap2, cpx_st, or_intror/
   | >iter_SO >iter_n_Sm //
   ]
 ]