-lemma teqx_rex_div (R): ∀T1,T2. T1 ≛ T2 →
- ∀L1,L2. L1 ⪤[R,T2] L2 → L1 ⪤[R,T1] L2.
-/3 width=5 by teqx_rex_conf, teqx_sym/ qed-.
+lemma teqx_rex_div (R):
+ ∀T1,T2. T1 ≛ T2 →
+ ∀L1,L2. L1 ⪤[R,T2] L2 → L1 ⪤[R,T1] L2.
+/3 width=5 by teqx_rex_conf_sn, teqx_sym/ qed-.