X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_succ.ma;h=b642bc56ba9109fab574af9db164bd59f9238d4c;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=8f8fe4047d04d994e09b49e8b60f1bbfeb32ca1b;hpb=888840f6b3a71d3d686b53b702d362ab90ab0038;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
index 8f8fe4047..b642bc56b 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
@@ -39,7 +39,7 @@ qed.
 lemma ysucc_inf: ∞ = ↑(∞).
 // qed.
 
-(* Inversion lemmas *********************************************************)
+(* Inversions ***************************************************************)
 
 (*** ysucc_inv_inj_sn *)
 lemma eq_inv_inj_ysucc (n1) (x2):
@@ -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-.
@@ -96,7 +96,7 @@ qed-.
 lemma eq_inv_ysucc_zero (x): ↑x = 𝟎 → ⊥.
 /2 width=2 by eq_inv_zero_ysucc/ qed-.
 
-(* Eliminators **************************************************************)
+(* Eliminations *************************************************************)
 
 (*** ynat_ind *)
 lemma ynat_ind_succ (Q:predicate …):