X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_sor_sor.ma;h=c52154795c318fb25de1a7e79e2e2e9dcf3d4890;hb=873fb39bdd21aa14877bf5d50db26e3a050c6d43;hp=ef667fd7ebfcf530096c8efdaedace0445af1bfd;hpb=503500ff9a6d9cca363a42b5fe7f3f5de69239f9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma
index ef667fd7e..c52154795 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_sor.ma".
 
 (*** sor_mono *)
 corec theorem pr_sor_mono:
-              ∀f1,f2,x,y. f1 ⋓ f2 ≘ x → f1 ⋓ f2 ≘ y → x ≡ y.
+              ∀f1,f2,x,y. f1 ⋓ f2 ≘ x → f1 ⋓ f2 ≘ y → x ≐ y.
 #f1 #f2 #x #y * -f1 -f2 -x
 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #H
 [ cases (pr_sor_inv_push_bi … H … H1 H2)