lfpx_drops completed!

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

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 e7ea1927d570991436d73f5f9e0e12c906077214..cb5ede22b61de36de2ab149c6d9711148486000a 100644 (file)
--- 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