X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_after.ma;h=a28f7b384a76697ad88453e5b109db45731a4b2e;hb=98fbba1b68d457807c73ebf70eb2a48696381da4;hp=4ca5caf746694bedf22ee49ee1ee1cf5444a8a0b;hpb=f4e73c50acfc4ed453edd423c9bbe28af5dc9c4c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
index 4ca5caf74..a28f7b384 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
@@ -1,3 +1,4 @@
+
 (**************************************************************************)
 (*       ___                                                              *)
 (*      ||M||                                                             *)
@@ -336,8 +337,8 @@ qed.
 (* Properties on uni ********************************************************)
 
 lemma after_uni: ∀n1,n2. 𝐔❴n1❵ ⊚ 𝐔❴n2❵ ≡ 𝐔❴n1+n2❵.
-@nat_elim2
-/4 width=5 by after_uni_next2, after_isid_sn, after_isid_dx, after_next/
+@nat_elim2 [3: #n #m <plus_n_Sm ] (**) (* full auto fails *)
+/4 width=5 by after_uni_next2, after_isid_dx, after_isid_sn, after_next/
 qed.
 
 (* Forward lemmas on at *****************************************************)