X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fltc.ma;h=9c2e12a7a5884231bec92e7d7cfad5f73b1015f7;hb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;hp=1d08fb15d98b9bd7af24e7d55f3ed133c8eea363;hpb=6604a232815858a6c75dd25ac45abd68438077ff;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
index 1d08fb15d..9c2e12a7a 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
@@ -12,10 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/insert_eq/insert_eq_1.ma".
+include "ground/generated/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) →