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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma
index a97d13067..edc241fc0 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma
@@ -19,7 +19,7 @@ include "ground/arith/nat_minus.ma".
 include "ground/arith/nat_lt.ma".
 include "ground/relocation/fr2_map.ma".
 
-(* RELATIONAL SUBTRACTION FOR FINITE RELOCATION MAPS WITH PAIRS *******************************************)
+(* RELATIONAL SUBTRACTION FOR FINITE RELOCATION MAPS WITH PAIRS *************)
 
 (*** minuss *)
 inductive fr2_minus: nat → relation fr2_map ≝
@@ -38,7 +38,7 @@ interpretation
   "minus (finite relocation maps with pairs)"
   'RMinus f1 i f2 = (fr2_minus i f1 f2).
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** minuss_inv_nil1 *)
 lemma fr2_minus_inv_nil_sn (f2) (i):