X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_after.ma;h=4ca5caf746694bedf22ee49ee1ee1cf5444a8a0b;hb=f4e73c50acfc4ed453edd423c9bbe28af5dc9c4c;hp=f202aa02becab61e1e59cf816ed05eca659b2aee;hpb=926796df5884453d8f0cf9f294d7776d469ef45b;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 f202aa02b..4ca5caf74 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
@@ -270,8 +270,10 @@ lemma after_mono_eq: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1,g2,g. g1 ⊚ g2 ≡ g
 lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → 
                  f1 ⊚ f2 ≡ f → ⫱*[n]f1 ⊚ f2 ≡ ⫱*[n]f.
 #n elim n -n //
-#n #IH #f1 #f2 #f #Hf1 #Hf cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ]
-#g1 #Hg1 #H1 cases (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/
+#n #IH #f1 #f2 #f #Hf1 #Hf
+cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
+cases (after_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
+<tls_xn <tls_xn /2 width=1 by/
 qed.
 
 (* Properties on isid *******************************************************)
@@ -412,10 +414,10 @@ lemma after_uni_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
   elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
   [ #g2 #j1 #Hg2 #H1 #H2 destruct
     elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   | #g2 #Hg2 #H2 destruct
     elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   ]
 ]
 qed.
@@ -448,10 +450,10 @@ lemma after_uni_succ_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
   elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
   [ #g2 #j1 #Hg2 #H1 #H2 destruct
     elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   | #g2 #Hg2 #H2 destruct
     elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   ]
 ]
 qed.