]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq_eq.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / gr_tl_eq_eq.ma
index 015d05d65d34c5143fb5db22026976baacfdf772..3322574e12abbf03b5b2611f8cafeceb3f01c447 100644 (file)
@@ -14,9 +14,9 @@
 
 include "ground/relocation/gr_tl_eq.ma".
 
-(* TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TAIL FOR GENERIC RELOCATION MAPS *****************************************)
 
-(* Main properties with gr_eq **********************************************************)
+(* Main constructions with gr_eq ********************************************)
 
 (*** eq_trans *)
 corec theorem gr_eq_trans: Transitive … gr_eq.