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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
index 4c141a301..c158f2593 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
@@ -89,7 +89,7 @@ qed-.
 
 (* Specific properties on coafter *******************************************)
 
-corec lemma coafter_total_aux: ∀f2,f1,f. f2 ~∘ f1 = f → f2 ~⊚ f1 ≡ f.
+corec lemma coafter_total_aux: ∀f2,f1,f. f2 ~∘ f1 = f → f2 ~⊚ f1 ≘ f.
 * #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
 [ cases n1 -n1
   [ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by coafter_refl, eq_f2/
@@ -99,5 +99,5 @@ corec lemma coafter_total_aux: ∀f2,f1,f. f2 ~∘ f1 = f → f2 ~⊚ f1 ≡ f.
 ]
 qed-.
 
-theorem coafter_total: ∀f2,f1. f2 ~⊚ f1 ≡ f2 ~∘ f1.
+theorem coafter_total: ∀f2,f1. f2 ~⊚ f1 ≘ f2 ~∘ f1.
 /2 width=1 by coafter_total_aux/ qed.