X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Fltc.ma;h=e5ea2770d22e50d9e7d9015d852ec8c19e8dadf1;hp=4bfd5c7c7fa1a867409da82b14622d09c7e94151;hb=258d2e384e8bf7008d2fb01c7d3fee5126d65120;hpb=2f20aaf586f7cb4fd2933d765f4d09fcf077e4c5

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
index 4bfd5c7c7..e5ea2770d 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
@@ -77,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-.