+
+(* 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-.