X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_coafter.ma;h=cb5ede22b61de36de2ab149c6d9711148486000a;hb=0c7cb3c503c0fcab104ad89ebc88683dc9830d06;hp=e7ea1927d570991436d73f5f9e0e12c906077214;hpb=5b93ea047903b606979705ed25a6df6504fd027c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
index e7ea1927d..cb5ede22b 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
@@ -611,7 +611,7 @@ elim (Hg1 0) #n #Hn
 qed-.
 
 fact coafter_isfin2_fwd_aux: (∀f1. @⦃0, f1⦄ ≡ 0 → H_coafter_isfin2_fwd f1) →
-                            ∀i2,f1. @⦃0, f1⦄ ≡ i2 → H_coafter_isfin2_fwd f1.
+                             ∀i2,f1. @⦃0, f1⦄ ≡ i2 → H_coafter_isfin2_fwd f1.
 #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
 #i2 #IH #f1 #H1f1 #f2 #Hf2 #H2f1 #f #Hf
 elim (at_inv_pxn … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1