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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
index 12ce1a69c..71a256c10 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
@@ -63,5 +63,5 @@ qed.
 (* Main inversions **********************************************************)
 
 (*** after_inv_total *)
-lemma pr_after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
+lemma pr_after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≐ f.
 /2 width=4 by pr_after_mono/ qed-.