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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isf.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isf.ma
index ebd461dcf..20d861a48 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isf.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isf.ma
@@ -18,13 +18,13 @@ include "ground/relocation/gr_ist_tls.ma".
 include "ground/relocation/gr_coafter_nat_tls.ma".
 include "ground/relocation/gr_coafter_isi.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
 (*** H_coafter_isfin2_fwd *)
 definition H_gr_coafter_des_ist_isf: predicate gr_map ≝
            λf1. ∀f2. 𝐅❪f2❫ → 𝐓❪f1❫ → ∀f. f1 ~⊚ f2 ≘ f →  𝐅❪f❫.
 
-(* Forward lemmas with ist and isf *)
+(* Destructions with gr_ist and gr_isf **************************************)
 
 (*** coafter_isfin2_fwd_O_aux *)
 fact gr_coafter_des_ist_isf_unit_aux:
@@ -51,7 +51,7 @@ fact gr_coafter_des_ist_isf_aux:
 elim (gr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
 elim (gr_coafter_inv_next_sn … Hf … H1) -Hf #g #Hg #H0
 lapply (IH … Hg1 … Hg) -i2 -Hg
-/2 width=4 by gr_ist_inv_next, gr_isf_push/ (**) (* full auto fails *)
+/2 width=4 by gr_ist_inv_next, gr_isf_push/ (* * full auto fails *)
 qed-.
 
 (*** coafter_isfin2_fwd *)