#R #I #L1 #L2 #V1 #V2 #s #H elim H -L2
/3 width=4 by rex_sort, rexs_step_dx, inj/
qed.
lemma rexs_pair: ∀R. (∀L. reflexive … (R L)) →
∀I,L1,L2,V. L1 ⪤*[R,V] L2 →
#R #I #L1 #L2 #V1 #V2 #s #H elim H -L2
/3 width=4 by rex_sort, rexs_step_dx, inj/
qed.
lemma rexs_pair: ∀R. (∀L. reflexive … (R L)) →
∀I,L1,L2,V. L1 ⪤*[R,V] L2 →