update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / ltc.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
index 1d08fb15d98b9bd7af24e7d55f3ed133c8eea363..9c2e12a7a5884231bec92e7d7cfad5f73b1015f7 100644 (file)
--- 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) →