X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Fltc.ma;h=e5ea2770d22e50d9e7d9015d852ec8c19e8dadf1;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=27ef34de4a87509def939141ac20c87ba8def7ae;hpb=54c4e854515cbcb1376881e9aedad006bf6545f2;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
index 27ef34de4..e5ea2770d 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/insert_eq/insert_eq_0.ma".
 include "ground_2/lib/functions.ma".
 
 (* LABELLED TRANSITIVE CLOSURE **********************************************)
@@ -37,7 +38,7 @@ lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f →
                  (∀a,b1. R a b1 b2 → Q a b1) →
                  (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
                  ∀a,b1. ltc … f … R a b1 b2 → Q a b1.
-#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq … b2)
+#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq_0 … b2)
 #b0 #H elim H -a -b1 -b0 /2 width=2 by/
 #a1 #a2 #b1 #b #b0 #H #Hb2 #_
 generalize in match Hb2; generalize in match a2; -Hb2 -a2
@@ -48,7 +49,7 @@ lemma ltc_ind_dx (A) (f) (B) (R) (Q:A→predicate B) (b1): associative … f →
                  (∀a,b2. R a b1 b2 → Q a b2) →
                  (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
                  ∀a,b2. ltc … f … R a b1 b2 → Q a b2.
-#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq … b1)
+#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq_0 … b1)
 #b0 #H elim H -a -b0 -b2 /2 width=2 by/
 #a1 #a2 #b0 #b #b2 #Hb0 #H #IHb0 #_
 generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0 -Hb0 -a1
@@ -76,3 +77,13 @@ lemma ltc_ind_dx_refl (A) (i) (f) (B) (R) (Q:A→predicate B) (b1):
 @(ltc_ind_dx … R … H1f … IH2 … H) -a -b2 -H1f #a #b2 #Hb12
 >(H2f a) -H2f /3 width=4 by ltc_rc/
 qed-.
+
+(* Properties with lsub *****************************************************)
+
+lemma ltc_lsub_trans: ∀A,f. associative … f →
+                      ∀B,C,R,S. (∀n. lsub_trans B C (λL. R L n) S) →
+                      ∀n. lsub_trans B C (λL. ltc A f … (R L) n) S.
+#A #f #Hf #B #C #R #S #HRS #n #L2 #T1 #T2 #H
+@(ltc_ind_dx … Hf ???? H) -n -T2
+/3 width=5 by ltc_dx, ltc_rc/
+qed-.