X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_coafter.ma;h=2d1d860f920d593b6985c5f427da321d73147e08;hb=86d7622f88247d83b2c366a722d2994a4af91929;hp=44f491de5f8e4a4879c74e80a55ad9ab14bb6812;hpb=b7de6afb9d3260ffea86ddf824e497419e1b56fb;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 44f491de5..2d1d860f9 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
@@ -694,7 +694,7 @@ lemma coafter_sor: ∀f. 𝐅⦃f⦄ → ∀f2. 𝐓⦃f2⦄ → ∀f1. f2 ~⊚
 [ #f #Hf #f2 #Hf2 #f1 #Hf #f1a #f1b #Hf1
   lapply (coafter_fwd_isid2 … Hf ??) -Hf // #H2f1
   elim (sor_inv_isid3 … Hf1) -Hf1 //
-  /3 width=5 by coafter_isid_dx, sor_refl, ex3_2_intro/
+  /3 width=5 by coafter_isid_dx, sor_idem, ex3_2_intro/
 | #f #_ #IH #f2 #Hf2 #f1 #H1 #f1a #f1b #H2
   elim (coafter_inv_xxp … H1) -H1 [1,3: * |*: // ]
   [ #g2 #g1 #Hf #Hgf2 #Hgf1