X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream_sor.ma;h=595a23a12509ce64f164ab6b832a23caae503e93;hb=75f395f0febd02de8e0f881d918a8812b1425c8d;hp=1605616646483a06265935f3601b75603943e0d1;hpb=d59f344b1e4b377e2f06abd9f8856d686d21b222;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sor.ma
index 160561664..595a23a12 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sor.ma
@@ -23,4 +23,4 @@ interpretation "union (nstream)"
 
 (* Specific properties on sor ***********************************************)
 
-axiom sor_total: ∀f1,f2. f1 ⋓ f2 ≡ f1 ∪ f2.
+axiom sor_total: ∀f1,f2. f1 ⋓ f2 ≘ f1 ∪ f2.