X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_after.ma;h=cc067a24d4284c57021d0c5231e88169b1d79f72;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=97636d5d88d40d57f9ffcb8c5b7e881bbc1b1990;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;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 97636d5d8..cc067a24d 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
@@ -166,7 +166,7 @@ corec lemma after_eq_repl_back2: ∀f1,f. eq_repl_back (λf2. f2 ⊚ f1 ≘ f).
 #f21 #f1 #f #g21 [1,2: #g1 ] #g #Hf #H21 [1,2: #H1 ] #H #g22 #H0
 [ cases (eq_inv_px …  H0 …  H21) -g21 /3 width=7 by after_refl/
 | cases (eq_inv_px …  H0 …  H21) -g21 /3 width=7 by after_push/
-| cases (eq_inv_nx …  H0 …  H21) -g21 /3 width=5 by after_next/ 
+| cases (eq_inv_nx …  H0 …  H21) -g21 /3 width=5 by after_next/
 ]
 qed-.
 
@@ -267,7 +267,7 @@ lemma after_mono_eq: ∀f1,f2,f. f1 ⊚ f2 ≘ f → ∀g1,g2,g. g1 ⊚ g2 ≘ g
 
 (* Properties on tls ********************************************************)
 
-lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≘ n → 
+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