propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / ynat_succ.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
index 8f8fe4047d04d994e09b49e8b60f1bbfeb32ca1b..9e4fb430cf71182640720323b20ffb472c656b25 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
@@ -72,7 +72,7 @@ lemma eq_inv_ysucc_bi: injective … ysucc.
 #x1 @(ynat_split_nat_inf … x1) -x1
 [ #n1 #x2 <ysucc_inj #H
   elim (eq_inv_inj_ysucc … H) -H #n2 #H1 #H2 destruct
-  /3 width=1 by eq_inv_nsucc_bi, eq_f/
+  <(eq_inv_nsucc_bi … H2) -H2 //
 | #x2 #H <(eq_inv_inf_ysucc … H) -H //
 ]
 qed-.