X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_ist_ist.ma;h=cfa6aaa918a313b8797309410ab3884bc157ee1a;hp=f80e08496bb384ba4b58a0d895139fc2c489aed1;hb=2ed8d2abcc3b0687141b627061b63350a0b200bd;hpb=b367de0252e88d6b0476648d5ceac7e4aeffca27

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_ist.ma
index f80e08496..cfa6aaa91 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_ist.ma
@@ -17,9 +17,9 @@ include "ground/relocation/gr_pat_lt.ma".
 include "ground/relocation/gr_pat_pat.ma".
 include "ground/relocation/gr_ist.ma".
 
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Advanced properties on at ************************************************)
+(* Advanced constructions with gr_pat ***************************************)
 
 (*** at_dec *)
 lemma gr_pat_dec (f) (i1) (i2): 𝐓❪f❫ → Decidable (@❪i1,f❫ ≘ i2).
@@ -41,7 +41,7 @@ lapply (dec_plt (λi1.@❪i1,f❫ ≘ i2) … (↑i2)) [| * ]
 ]
 qed-.
 
-(* Main forward lemmas on at ************************************************)
+(* Main destructions with gr_pat ********************************************)
 
 (*** at_ext *)
 corec theorem gr_eq_ext_pat (f1) (f2): 𝐓❪f1❫ → 𝐓❪f2❫ →