X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fltc.ma;h=c0d091c3c32129f8e5a3a449a88b45f56c1a1a34;hp=1d08fb15d98b9bd7af24e7d55f3ed133c8eea363;hb=ae626612bff9c3746dd7647bbada791c737e348c;hpb=4d232392091ee233afc26ecf3120dd5f5c6a33c8

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
index 1d08fb15d..c0d091c3c 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
@@ -15,7 +15,7 @@
 include "ground/insert_eq/insert_eq_1.ma".
 include "ground/lib/functions.ma".
 
-(* LABELLED TRANSITIVE CLOSURE **********************************************)
+(* LABELLED TRANSITIVE CLOSURE FOR RELATIONS ********************************)
 
 inductive ltc (A:Type[0]) (f) (B) (R:relation3 A B B): relation3 A B B ≝
 | ltc_rc   : ∀a,b1,b2. R a b1 b2 → ltc … a b1 b2
@@ -56,7 +56,7 @@ generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0
 elim H -a2 -b -b2 /4 width=4 by ltc_trans/
 qed-.
 
-(* Advanced elimiations with reflexivity ************************************)
+(* Advanced eliminations (with reflexivity) *********************************)
 
 lemma ltc_ind_sn_refl (A) (i) (f) (B) (R) (Q:relation2 A B) (b2):
                       associative … f → right_identity … f i → reflexive B (R i) →