update in ground_2 and basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
index 4bfd5c7c7fa1a867409da82b14622d09c7e94151..e5ea2770d22e50d9e7d9015d852ec8c19e8dadf1 100644 (file)
--- 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-.