]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_compose.ma
index 4cd185f2a692c566e4b16001eee76119a474fe59..12ce1a69c4ae4151886ac7ce9672a15221b4eeea 100644 (file)
@@ -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