first definition of cpm:

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_after.ma

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 4ca5caf746694bedf22ee49ee1ee1cf5444a8a0b..a28f7b384a76697ad88453e5b109db45731a4b2e 100644 (file)
--- 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 *****************************************************)