-lemma lex_ltc_step_dx: ∀R. c_reflexive … R → s_rs_transitive … R (λ_. lex R) →
- ∀L1,L. lex (LTC … R) L1 L →
- ∀L2. lex R L L2 → lex (LTC … R) L1 L2.
-/4 width=3 by lex_ltc, lex_inv_ltc, step/ qed-.
+lemma lex_CTC_step_dx: ∀R. c_reflexive … R → s_rs_transitive … R (λ_. lex R) →
+ ∀L1,L. lex (CTC … R) L1 L →
+ ∀L2. lex R L L2 → lex (CTC … R) L1 L2.
+/4 width=3 by lex_CTC, lex_inv_CTC, step/ qed-.