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=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3;hp=4cd185f2a692c566e4b16001eee76119a474fe59;hpb=835d26af0fdaa835b6aa1b35765cb22fb3590c4b;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 4cd185f2a..71a256c10 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
@@ -28,7 +28,7 @@ interpretation
   "functional composition (partial relocation maps)"
   'compose f2 f1 = (pr_compose f2 f1).
 
-(* Basic constructions (specific) *******************************************)
+(* Basic constructions ******************************************************)
 
 lemma pr_compose_unfold_refl (f2) (f1): ⫯(f2∘f1) = (⫯f2)∘(⫯f1).
 #f2 #f1
@@ -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-.