partial update in static_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma
index 7ee376ea1b0e554d29904d45275ddd4ceb5ff95b..9d4997f10777e01ae8d3e053e0bbdcae593830d1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma
@@ -17,7 +17,7 @@ include "ground/relocation/pr_pat_pat_id.ma".
 
 (* IDENTITY CONDITION FOR PARTIAL RELOCATION MAPS ***************************)
 
-(* Advanced constructions with pr_isi ***************************************)
+(* Advanced constructions with pr_isi and pr_pat ****************************)
 
 (*** isid_at *)
 lemma pr_isi_pat (f): (∀i. @❪i,f❫ ≘ i) → 𝐈❪f❫.