#R #HR #L1 #T #R0 #HL1 #IHL1 #L2 #HL12
@(TC_star_ind … HL1 IHL1 … HL12) /2 width=1 by lfxs_refl/
qed-.
lemma tc_lfxs_ind_dx: ∀R. (∀L. reflexive … (R L)) →
∀L2,T. ∀R0:predicate …. R0 L2 →
#R #HR #L1 #T #R0 #HL1 #IHL1 #L2 #HL12
@(TC_star_ind … HL1 IHL1 … HL12) /2 width=1 by lfxs_refl/
qed-.
lemma tc_lfxs_ind_dx: ∀R. (∀L. reflexive … (R L)) →
∀L2,T. ∀R0:predicate …. R0 L2 →