update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_compose.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
index 4cd185f2a692c566e4b16001eee76119a474fe59..71a256c103633dbe7cacf85dca2c43f326c72a1a 100644 (file)
--- 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: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89¡ f.
+lemma pr_after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89\90 f.
 /2 width=4 by pr_after_mono/ qed-.