]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / gr_coafter_nat_tls.ma
index f297468f9bc80fb0c2be569210e3071e70d2d9a7..6d953f203f9ea589f749d216d70a8572cbff5503 100644 (file)
@@ -16,9 +16,9 @@ include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_nat.ma".
 include "ground/relocation/gr_coafter.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with nat and iterated tail ********************************************)
+(* Constructions with gr_nat and gr_tls *************************************)
 
 (*** coafter_tls *)
 lemma gr_coafter_tls_bi_tls (n2) (n1):